Email Gateway (Aug 19 2022 at 10:11): Email Gateway (Aug 19 2022 at 10:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 10:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 10:12):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
cTest.thy
cTest_doc.pdf
Last updated: Apr 19 2024 at 04:17 UTC