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
Description: Adobe PDF document



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.