Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Replies: 20   Last Post: Mar 19, 2013 1:32 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: I Bet \$25 to your \$1 (PayPal) That You Can’t P
rove Naive Set Theory Inconsistent

Posted: Mar 14, 2013 4:34 AM

On Mar 14, 5:39 pm, Jan Burse <janbu...@fastmail.fm> wrote:
> Graham Cooper schrieb:
>

> > If TRUE(x)  doesn't work, what is NOT(NOT(x)) ??
>
> When modeling inferences, especially in Prolog, I
> usually prefer the following verbs:
>
>      solve/1: Like in the vanilla interpreter for
>             Prolog
>      thm/1: Like many logical frameworks do.
>      pos/1 and neg/1: If you have polarity.

where does proof() fit in?

*TRACE MODE* ?

>
> Using true/1 is not wrong, but it has the Tarski
> limitation like the other verbs, and any verb you
> would use, always have.
>

> > This doesn't mean that you Graham Cooper,
> > with your Prolog, cannot derive some
> > truths. But you will not be able to derive
> > all truths.

>
> Right? Except for propositional logic, where
> you can build complete inference engines, as
> soon as you have a little FOL, nada.

What is un-provable?

un-thm(...)

neg(...)

----------

All theorems are by definition proven,

hence there is no such predicate proof()

but there is such predicate true() or thm()

similar to not()

PROOF() is just more verbose than TRU()

**********************

HUMAN> thm( 1+1=2 ) ?

PROLOG> YES

----------------------

HUMAN> prove( 1+1=2 ) ?

PROLOG>
*TRACE MODE*
X=s(0)
Y=0
Z=s(0)
YES

Herc

Date Subject Author
3/13/13 Graham Cooper
3/13/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/14/13 Charlie-Boo
3/14/13 Graham Cooper
3/15/13 Charlie-Boo
3/19/13 Graham Cooper
3/19/13 Charlie-Boo
3/19/13 Charlie-Boo
3/15/13 Graham Cooper
3/15/13 Charlie-Boo
3/15/13 Graham Cooper
3/19/13 Charlie-Boo