# Re: [isabelle] Important axiom question: can (seS q P) occur in (P x)?

```So I defined a function which can reference itself like:

function PT :: "sT => bool" where
"PT x = (x NOTIN {{0}. PT})"
by(auto)

```
To prove the inconsistency, I had to use "sorry" to restate the definition of the function as a theorem, Sledgehammer wouldn't prove it, and it's a simple restatement of a definition, so I don't know why it can't be proved:
```
theorem PT_formula:
"PT x = (x NOTIN {{0}. PT})"
sorry

I then proved a theorem which basically says:

"(u IN {u}) & (u NOTIN u) --> (u IN u)"

where (u NOTIN u) is the application of my function (PT u).

```
The only question is about whether the theorem "PT_formula" having a problem being proved means anything.
```
```
I attach the theory, at about 80 lines, and I attach the PDF, if someone wants to look at it and tell me if it means anything, which I assume it does. It at least means that Goldrei in "Classic Set Theory for Guided Independent Study" left out an important point that Drake didn't in "Intermediate Set Theory".
```
Regards,
GB

On 2/14/2013 5:09 PM, Gottfried Barrow wrote:
```
No one probably has time for this, but for myself, for the problem I described, I'm trying answer why I can't do this:
```
```
"Define a function P::(sT => bool) such that (P == (%x. ...~(x IN seS q P)...))".
```
```
The "..." is any additional formula, and the function seS is a constant that's only defined by its use in the axiom. If I can do that, then I'm doomed.
```
Thanks,
GB

On 2/14/2013 2:37 PM, Gottfried Barrow wrote:
```
```Hi,

```
Axioms are to be feared, so I ask this question. There is the general FOL formula which I modify, but given here unmodified:
```
!q. ?r. !x. (x IN r <-> (x IN q & phi(x))),

```
where it is required that r not occur in the formula phi(x), and where phi(x) is a FOL formula with a free variable x.
```
I implement it like this:

!q. !P. !x. ( x IN (seS q P) <-> (x IN q & (P x)))

The question becomes, "Can the term (seS q P) occur in (P x)?"

The function and types are as follows:

typedecl sT
q, x :: sT
P::(sT => bool)
consts seS :: "(sT => (sT => bool) => sT)"
consts IN :: "sT => sT => bool"

```
It seems like things would get circular, but then maybe there's a recursive way to do it.
```
```
If it can be done, how would I specify that (seS q P) not be allowed in (P x)?
```
Thanks,
GB

```
```

```
```
```
```(*--"\<^bold>C\<^bold>O\<^bold>U\<^bold>N\<^bold>T\<^bold>E\<^bold>R\<^bold>X (cTest)"*)

theory cTest
imports Complex_Main
begin

typedecl sT

consts inP :: "sT => sT => bool" (infixl "\<in>\<^isub>\<iota>" 55)

abbreviation niP :: "sT => sT => bool" (infixl "\<notin>\<^isub>\<iota>"  55) where
"niP p q == \<not>(p \<in>\<^isub>\<iota> q)"

axiomatization where
Ax_x\<^isup>N: "(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> x \<in>\<^isub>\<iota> s) \<longleftrightarrow> r = s"

consts emS :: "sT" ("\<emptyset>")

axiomatization where
Ax_emS: "(x \<notin>\<^isub>\<iota> \<emptyset>)"

consts paS :: "sT => sT => sT"

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
translations
"\<lbrace>r,s\<rbrace>" == "CONST paS r s"

axiomatization  where
Ax_paS: "x \<in>\<^isub>\<iota> \<lbrace>r,s\<rbrace> \<longleftrightarrow> (x = r \<or> x = s)"

theorem paS_is_unique:
"(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> (x = p \<or> x = q)) \<longleftrightarrow> r = \<lbrace>p,q\<rbrace>"
by(metis Ax_x\<^isup>N Ax_paS)

definition siS :: "sT => sT" where
"siS r = paS r r"
notation
siS  ("(\<lbrace>(_)\<rbrace>)")

theorem siS_is_unique:
"(\<forall>x. x \<in>\<^isub>\<iota> r \<longleftrightarrow> x = s) \<longleftrightarrow> r = \<lbrace>s\<rbrace>"
by(metis
siS_def
paS_is_unique)

consts seS :: "sT => (sT => bool) => sT"

syntax
"_seS" :: "sT => (sT => bool) => sT" ("(\<lbrace>(_./ _)\<rbrace>)")
translations
"\<lbrace>q. P\<rbrace>" == "CONST seS q P"

axiomatization where
Ax_seS: "\<forall>q::sT. \<forall>P::(sT => bool). x \<in>\<^isub>\<iota> \<lbrace>q. P\<rbrace> \<longleftrightarrow> (x \<in>\<^isub>\<iota> q \<and> P x)"

function PT :: "sT => bool" where
"PT x = (x \<notin>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>)"
by(auto)

theorem PT_formula :
"PT x = (x \<notin>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>)"
sorry

theorem
"\<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<in>\<^isub>\<iota> \<lbrace> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<rbrace>  \<and> PT \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<longrightarrow> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace> \<in>\<^isub>\<iota> \<lbrace>\<lbrace>\<emptyset>\<rbrace>. PT\<rbrace>"
by(metis
Ax_seS
siS_is_unique
PT_formula)
--"Metis: The assumptions are inconsistent"

(*
For phi(x) = x \<notin>\<^isub>\<iota> u, state the following axiom per the normal axiom scheme,
as if it let u occur in phi(x):
\<forall>q.\<exists>u.\<forall>x. (x \<in>\<^isub>\<iota> q \<and> x \<notin>\<^isub>\<iota> u) \<longleftrightarrow> x \<in>\<^isub>\<iota> u.
Now, let q = \<lbrace>\<emptyset>\<rbrace> and u = \<emptyset>. So
(\<emptyset> \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> \<emptyset> \<notin>\<^isub>\<iota> \<emptyset>) \<longrightarrow> \<emptyset> \<in>\<^isub>\<iota> \<emptyset>.
ISAR:
axiomatization where
PT_axiom:
"\<forall>q.\<exists>u.\<forall>x. (x \<in>\<^isub>\<iota> q \<and> x \<notin>\<^isub>\<iota> u) \<longleftrightarrow> x \<in>\<^isub>\<iota> u"
theorem
"(\<emptyset> \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> \<emptyset> \<notin>\<^isub>\<iota> \<emptyset>) \<longrightarrow> \<emptyset> \<in>\<^isub>\<iota> \<emptyset>"
by(metis (full_types) PT_axiom)
theorem
"(a \<in>\<^isub>\<iota> \<lbrace>a\<rbrace> \<and> a \<notin>\<^isub>\<iota> a) \<longrightarrow> a \<in>\<^isub>\<iota> a"
by(metis (full_types) PT_axiom)
*)

(*
function consist_test_1 :: "sT => bool" where
"consist_test_1 x = (x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1))"
by(auto)

theorem consist_test_1_formula :
"consist_test_1 x = (x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1))"
sorry

theorem consist_test_1_iff:
"\<forall>x. x \<in>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1) \<longleftrightarrow> (x \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> consist_test_1 x)"
apply simp
by(metis
Ax_seS
consist_test_1_formula)

theorem
"\<forall>x. ~(x \<in>\<^isub>\<iota> \<lbrace>\<emptyset>\<rbrace> \<and> consist_test_1 x)"
apply(simp)
by(metis
Ax_seS
consist_test_1_formula)

theorem
"\<forall>x. x \<notin>\<^isub>\<iota> (seS \<lbrace>\<emptyset>\<rbrace> consist_test_1)"
by(metis
Ax_seS
consist_test_1_formula)
*)

end
--"\<^bold>[\<^bold>\<Theta>\<^bold>]"

```

Attachment: cTest_doc.pdf