|
|
Re: Peano-like Axioms for the Integers in DC Proof
Posted:
Mar 3, 2013 6:13 PM
|
|
On Mar 1, 2:50 pm, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Thursday, February 28, 2013 7:20:42 PM UTC-5, Graham Cooper wrote:
>
> [snip]
>
> > Ah ok. Can you post the proof of Induction formula or is it part of
>
> > the 1000 lines of formal stuff?
>
> I derived the induction formula for integers using well over 1,000 lines in the DC Proof format. In my previous thread here, I posted the text of a proof that derived the induction formula for natural numbers (only about 100 lines) starting with a single injective function defined on a set.
>
> I am currently trying to derive integer addition -- at least another 1,000 lines, and much more complicated. When (if?)I finish that, I will include all of these proofs in their entirety in the samples downloaded with DC Proof. I will also post key parts of it here and at my math blog for discussion.
>
>
>
> > I'm guessing you used Axiom Of Extensionality.
>
> So far, I haven't had to use what I call the Set Equality Axiom (Extensionality in ZFC) in these proofs. I'm guessing I won't need it.
>
I'll see if I can work this set induction format into my Prolog set
theory. for NATS.
14 ALL(p):[Set(p)
& ALL(a):[a @ p => a @ z]
& 0 @ p
& ALL(a):[a @ p => next(a) @ p]
& ALL(a):[a @ p => next'(a) @ p]
=> ALL(a):[a @ z => a @ p]]
And that will finish Infinite Sets in PROLOG as its not necessary for
Logic in Natural Language
A(X)
X e S <-> p(X)
Like NAIVE SET THEORY, I use
e(A, nats) <- nat(A)
Now I can refer to the predicate nat AND it's variable, as a Set
(without the variable)
nat(0).
nat(s(X)) <- nat(X).
--------------------------
So although I cant formulate 2nd Order Induction
p(0)
A(x) p(x) -> p(s(x))
-----------------
A(x) p(x)
because I can't refer to the inside of a general predicate p(..[X]..)
I can do Quantifier Style formulas in Sets instead, since the argument
X is pre-stipulated here!
e(A, nats) <- nat(A)
--------------------
nat(A) is a 1OL predicate
nats is a 2OL set
-----------------------
e.g. finite subset will be
ss( S1, S2 ) <- e( @A , S1 ) , e( A , S2 )
intersection is
int( S1,S2) <- e(A, S1) , e(A, S2)
--------------------------
So I can already do:
~ A(X) p(X) <-> E(X) ~p(X)
with sets, without using Quantifier Syntax (referring to inside
general predicates)
not(ss(S1,S2)) <- int(S1, not(S2))
ss(S1,S2) is the same as ALL(X) XeS1 -> XeS2
and I have negation of Sets also
e( A , not(evens) ) <- e( A , odds)
So PROLOG can prove that NOT ALL NATS ARE EVEN
by doing SetWise operations, then calling
int( nats, odds)
and returning
s(0)
(a counterexample witness to the proof)
---------------
In Block Prolog, prefacing each VARAIBLE with @ will stand for ALL
solutions for that variable.
So PREDICATE INDUCTION might be:
p @N
p 0
if [p @N] [p [s N]]
@N means ALL(N) ... N...
------------------------
or using an inference rule
if [ and [ [ p 0 ] [ if [ p @N ] [ p [s N] ] ] [ p @ N]
--------------------------
But these are 2OL, predicates are all lowercase terms, not Variables.
No Query will match a theorem or predicate with 'p'.
So I will try Induction with your SET FORMULA as it's a higher level
Then I will abandon infinite sets for the foreseeable future so Prolog
can enumerate ALL(x) statements (which will be encoded as subset
statements)
Herc
--
www.BLoCKPROLOG.com
|
|
