|
|
Re: Peano-like Axioms for the Integers in DC Proof
Posted:
Feb 28, 2013 7:20 PM
|
|
On Mar 1, 6:30 am, Dan Christensen <Dan_Christen...@sympatico.ca>
wrote:
> On Sunday, February 24, 2013 5:21:55 PM UTC-5, Graham Cooper wrote:
>
> [snip]
>
> > Your system is INCONSISTENT!
>
> If it is, this is no proof.
>
>
>
>
>
>
>
>
>
>
>
> > > > Your system should be able to prove:
>
> > > > ~p & (~p -> p) -> ~p
>
> > > Easy.
>
> > > 1 ~P & [~P => P]
>
> > > Premise
>
> > > 2 ~P
>
> > > Split, 1
>
> > > 3 ~P & [~P => P] => ~P
>
> > > > In fact by modus ponens it is easy to see that p
>
> > > > derives from ~p & (~p -> p).
>
> > > Also easy.
>
> > > 1 ~P & [~P => P]
>
> > > Premise
>
> > > 2 ~P
>
> > > Split, 1
>
> > > 3 ~P => P
>
> > > Split, 1
>
> > > 4 P
>
> > > Detach, 3, 2
>
> > > 5 ~P & [~P => P] => P
>
> Really Graham, as you SHOULD know,absolutely anything follows from a falsehood. And ~P & [~P => P] is a falsehood. Make a truth table.
>
>
>
> > Really Dan there are dozens of Micro Data structures and fine grain
>
> > computing models, you are knocking the very System you modelled in a
>
> > convoluted syntax based on ZFC, a much larger framework than Peano
>
> > Arithmetic.
>
> Makes no sense to me. Sorry.
Ah ok. Can you post the proof of Induction formula or is it part of
the 1000 lines of formal stuff?
I'm guessing you used Axiom Of Extensionality.
Herc
--
www.BLoCKPROLOG.com
|
|
