# LX Layering Axiom : Experimental Version 4

## File ax4.otter

```     1	%
2	%   Another attempt.
3	%
4	%   This time, I'm using the ax2 style of sticking to rdf(_,_,_)
5	%   (which happens to keep the axioms in LX) and clausal form (or
6	%   nearly so), to reduce un-thought-of consequences.
7	%
8	%   I'm also starting with just negation and our truth predicate, so I
9	%   can see if I've got that truth predicate right.
10	%
11
12	set(prolog_style_variables).
13	formula_list(usable).
14
15	% needed for tests 1 and 2:
16
17	all T S P O DenS DenP DenO (
18	  rdf(T, rdf_type, lx_TrueSentence) &
19	  rdf(T, lx_subjectTerm, S) &
20	  rdf(T, lx_predicateTerm, P) &
21	  rdf(T, lx_objectTerm, O) &
22	  rdf(S, lx_denotation, DenS) &
23	  rdf(P, lx_denotation, DenP) &
24	  rdf(O, lx_denotation, DenO)
25	  ->
26	  rdf(DenS, DenP, DenO)
27	).
28
29	% the <- form is also true, if you move the unconstrained terms
30	% inside, but we don't need that yet.
31
32
33	% needed for test 3:
34
35	all F N (
36	  rdf(F, lx_negated, N) &
37	  rdf(F, rdf_type, lx_TrueSentence)
38	  ->
39	  -rdf(N, rdf_type, lx_TrueSentence)
40	).
41
42	all T S P O DenS DenP DenO (
43	  -rdf(T, rdf_type, lx_TrueSentence) &
44	  rdf(T, lx_subjectTerm, S) &
45	  rdf(T, lx_predicateTerm, P) &
46	  rdf(T, lx_objectTerm, O) &
47	  rdf(S, lx_denotation, DenS) &
48	  rdf(P, lx_denotation, DenP) &
49	  rdf(O, lx_denotation, DenO)
50	  ->
51	  -rdf(DenS, DenP, DenO)
52	).
53
54	% needed for 4:
55
56	all F N (
57	  rdf(F, lx_negated, N)
58	  ->
59	  rdf(N, lx_negated, F)
60	).
61
62	all F N (
63	  rdf(F, lx_negated, N) &
64	  -rdf(F, rdf_type, lx_TrueSentence)
65	  ->
66	  rdf(N, rdf_type, lx_TrueSentence)
67	).
68
69	% others we might want:
70
71	% all reified relations between objects exist; they may or may
72	% not be true...
73
74	% Manually Skolemized Form  (see ax4.lemma1.otter)
75
76	(all DenS DenP DenO (
77	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
78	      lx_subjectTerm, symFor(DenS)) &
79	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
80	      lx_predicateTerm, symFor(DenP)) &
81	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)),
82	      lx_objectTerm, symFor(DenO)) &
83	  rdf(symFor(DenS), lx_denotation, DenS) &
84	  rdf(symFor(DenP), lx_denotation, DenP) &
85	  rdf(symFor(DenO), lx_denotation, DenO)
86	)).
87
88
89	% the negation of every reified triple exists (whether true or not)
90
91	% Manually Skolemized Form  (see ax4.lemma2.otter)
92
93	(all T (
94	  (exists S (
95	    rdf(T, lx_subjectTerm, S)
96	  ))
97	  ->
98	  rdf(T, lx_negated, negation(T))
99	)).
100
102
103	all T S P O DenS DenP DenO (
104	  rdf(T, rdf_type, lx_FalseSentence) &
105	  rdf(T, lx_subjectTerm, S) &
106	  rdf(T, lx_predicateTerm, P) &
107	  rdf(T, lx_objectTerm, O) &
108	  rdf(S, lx_denotation, DenS) &
109	  rdf(P, lx_denotation, DenP) &
110	  rdf(O, lx_denotation, DenO)
111	  ->
112	  -rdf(DenS, DenP, DenO)
113	).
114
115	all T S (
116	  rdf(T, lx_subjectTerm, S)
117	  ->
118	  (
119	   rdf(T, rdf_type, lx_FalseSentence)
120	   |
121	   rdf(T, rdf_type, lx_TrueSentence)
122	  )
123	).
124
125	% A *description* of the sentence "this is false" is itself false,
126	% but even though the descriptions of all triple-sentence exist, the
127	% FOL sense of "all" there does not include self-referencing ones (see
128	% "occurs check").
```

## File ax4.lemma1.otter

```     1
2	set(auto).
3	clear(control_memory).
4	assign(max_mem, 768000).
5	set(prolog_style_variables).
6	formula_list(usable).
7
8
9	-(
10
11	% Manually Skolemized Form
12	(all DenS DenP DenO (
13	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_subjectTerm, symFor(DenS)) &
14	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_predicateTerm, symFor(DenP)) &
15	  rdf(triple(symFor(DenS), symFor(DenP), symFor(DenO)), lx_objectTerm, symFor(DenO)) &
16	  rdf(symFor(DenS), lx_denotation, DenS) &
17	  rdf(symFor(DenP), lx_denotation, DenP) &
18	  rdf(symFor(DenO), lx_denotation, DenO)
19	))
20
21	->
22
23	% Pretty form
24	(all DenS DenP DenO (
25	  exists T S P O (
26	    rdf(T, lx_subjectTerm, S) &
27	    rdf(T, lx_predicateTerm, P) &
28	    rdf(T, lx_objectTerm, O) &
29	    rdf(S, lx_denotation, DenS) &
30	    rdf(P, lx_denotation, DenP) &
31	    rdf(O, lx_denotation, DenO)
32	  )
33	))
34
35
36	).```

## File ax4.lemma2.otter

```     1
2	set(auto).
3	clear(control_memory).
4	assign(max_mem, 768000).
5	set(prolog_style_variables).
6	formula_list(usable).
7
8
9	-(
10
11	% Manually Skolemized Form
12	(all T (
13	  (exists S (
14	    rdf(T, lx_subjectTerm, S)
15	  ))
16	  ->
17	  rdf(T, lx_negated, negation(T))
18	))
19
20	->
21
22	% Pretty form
23	(all T (
24	  (exists S (
25	    rdf(T, lx_subjectTerm, S)
26	  ))
27	  ->
28	  (exists N (
29	    rdf(T, lx_negated, N)
30	  ))
31	))
32
33
34	).```

## File ax4-test0.otter

```     1
2
3	set(auto).
4	clear(control_memory).
5	assign(max_mem, 768000).
6	set(prolog_style_variables).
7
8	include('ax4.otter').
```

## File ax4-test1.otter

```     1	%
2	%  Given
3	%   l2 says rdf(a,b,c) is true.
4	%  1. are we satisfiable?
5	%  2. can we prove rdf(a,b,c)?
6	%
7
8	set(auto).
9	clear(control_memory).
10
11	include('ax4.otter').
12
13	formula_list(usable).
14
15	rdf(l2, rdf_type, lx_TrueSentence).
16	rdf(l2, lx_subjectTerm, l2s).
17	rdf(l2, lx_predicateTerm, l2p).
18	rdf(l2, lx_objectTerm, l2o).
19	rdf(l2s, lx_denotation, a).
20	rdf(l2p, lx_denotation, b).
21	rdf(l2o, lx_denotation, c).
22
23	% GOAL (be sure to terminate with SOS-empty when this is commented out)
24	-rdf(a,b,c).```

## File ax4-test2.otter

```     1	%
2	%  Given
3	%   l1 says l2 is true.
4	%   l2 says rdf(a,b,c) is true.
5	%  1. are we satisfiable?
6	%  2. can we prove rdf(a,b,c)?
7	%
8
9	set(auto).
10	clear(control_memory).
11
12	include('ax4.otter').
13
14	formula_list(usable).
15
16	rdf(l1, rdf_type, lx_TrueSentence).
17	rdf(l1, lx_subjectTerm, l1s).
18	rdf(l1, lx_predicateTerm, l1p).
19	rdf(l1, lx_objectTerm, l1o).
20	rdf(l1s, lx_denotation, l2).
21	rdf(l1p, lx_denotation, rdf_type).
22	rdf(l1o, lx_denotation, lx_TrueSentence).
23
24	% don't reify l2, just it's truth (above).  if we did, we'd be saying
25	%    l1 says (l2 is true and l2 says rdf(a,b,c) is true)
26
27	rdf(l2, lx_subjectTerm, l2s).
28	rdf(l2, lx_predicateTerm, l2p).
29	rdf(l2, lx_objectTerm, l2o).
30	rdf(l2s, lx_denotation, a).
31	rdf(l2p, lx_denotation, b).
32	rdf(l2o, lx_denotation, c).
33
34	% GOAL (be sure to terminate with SOS-empty when this is commented out)
35	-rdf(a,b,c).
```

## File ax4-test3.otter

```     1	%
2	%  Given
3	%   l1 says rdf(a,b,c) is false
4	%  1. are we satisfiable?
5	%  2. can we prove -rdf(a,b,c)?
6	%
7
8	set(auto).
9	clear(control_memory).
10
11	include('ax4.otter').
12
13	formula_list(usable).
14
15	rdf(l1, rdf_type, lx_TrueSentence).
16	rdf(l1, lx_negated, l2).
17
18	rdf(l2, lx_subjectTerm, l2s).
19	rdf(l2, lx_predicateTerm, l2p).
20	rdf(l2, lx_objectTerm, l2o).
21	rdf(l2s, lx_denotation, a).
22	rdf(l2p, lx_denotation, b).
23	rdf(l2o, lx_denotation, c).
24
25	% GOAL (be sure to terminate with SOS-empty when this is commented out)
26	%
27	rdf(a,b,c).
```

## File ax4-test4.otter

```     1	%
2	%  Given
3	%   l1 is the negation of l2
4	%   l2 says l1 is true
5	%   (neither is asserted)
6	%  1. are we satisfiable?
7	%
8	%  if not, good, but then the axioms shouldn't be satisfiable either.
9	%  -> some constructs, like this one, must be pre-created.
10	%
11
12	set(auto).
13	clear(control_memory).
14
15	include('ax4.otter').
16
17	formula_list(usable).
18
19	rdf(l1, lx_negated, l2).
20
21	rdf(l2, lx_subjectTerm, l2s).
22	rdf(l2, lx_predicateTerm, l2p).
23	rdf(l2, lx_objectTerm, l2o).
24	rdf(l2s, lx_denotation, l1).
25	rdf(l2p, lx_denotation, rdf_type).
26	rdf(l2o, lx_denotation, lx_TrueSentence).
27
28	% GOAL (be sure to terminate with SOS-empty when this is commented out)
29	%
30	%   l1 being true -> l2 being false
31	%   l2 being true -> l1 being false
32	%....
33
34	%what axioms are we missing for that?
```

Sandro Hawke
Generated Thu Aug 22 16:26:47 EDT 2002