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: PREDICATE CALCULUS 2
Replies: 23   Last Post: Nov 29, 2012 1:13 AM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Re: PREDICATE CALCULUS 2
Posted: Nov 27, 2012 5:14 PM

On Nov 28, 12:38 am, Dan Christensen <d...@dcproof.com> wrote:
> On Nov 25, 10:36 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>
>

> > Predicate Calculus only uses the  e(member,set)
> > predicate to construct set theoretic formula.

>
> > I convert ALL() Quantifiers to a SUBSET OF TERM Predicate
>
> > all(X,d(..X..),p(..X..))
> >    /\
> >    ||
> >    \/
> > {X|d(..X..)}  C  {X|p(..X..)}

>
> > Either formula can be converted to High Order Prolog.
>
> > HOP e.g.
>
> > all( X , less(X,3) , add( X, {1,2,3,4}, 4) )
> >  ^     ^       DOMAIN     SUPERSET
> >  |     |
> >  |    TERM
> >  |
> >  QUANTIFIER

>
> > All(X):X<3  X+{1,2,3 or 4}=5
> >    /\
> >    ||    LOGIC FORMULA
> >    ||
> >    \/
> > all( X , less(X,3) , add( X, {2,3,4}, 4) )       *HOP*
> >    /\
> >    ||
> >    ||    SET FORMULA
> >    \/
> > { X | less(X,3) }  C  { X | add(X, {1,2,3,4}, 4) }
> >    |
> >    |
> >    |    ELEMENTS
> >    \/
> > {0,1,2}  C  {0,1,2,3}
> >    |
> >    v
> > TRUE

>
> > Herc
> > --
> > if( if(t(S),f(R)) , if(t(R),f(S)) ).
> >     if it's sunny then it's not raining
> > ergo
> >        if it's raining then it's not sunny

>
> In your proposed system, how do you determine whether or not a given
> set of ordered pairs represents a function mapping one set to another?
> (You will probably need existential quantifiers.)
>
> Dan
>

Everything is Relational with multiple records for results.

Using Charlie Boo's system.

...

This happens to be a function by it's effective definition.

m n a
________
0 0 0
s(0) 0 s(0)
s(s(0)) 0 s(s(0))
...

where the BAR ____ means (m,n) tuples are unique.

...

But Prolog doesn't have uniqueness constraints, entire rows can be
duplicated and it's the same relation, like duplicating elements of a
set. The POST-PARSER may format the results by removing duplicates of
the final relation.

There is nothing stopping you adding a fact

Now (1,2) has 2 entries and is no longer a function.

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

1st you have to recognise which ALL(x) are merely ANY(x)

...

[PERSON]

ALL(s1) ALL(s2) s1 C s2 ^ s2 C s1
-> s1 = s2

...

[PERSON PREPARSES HIS LOGIC FORMULA]

ANY(s1) ANY(s2) s1 C s2 ^ s2 C s2
-> s1= s2

[FORMAL PROLOG PREPARSER]
S1 C S2 ^ S2 C S1
-> S1 = S2

if( and( c(S1,S2) , c(S2,S1)) , =(S1,S2) ).

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

It might look clumsy but
if( and(..,..) , ... )

is how most rules work, even the predicates themselves, by doing a
cartesian join on pairs of theorems.

I will do a new post on the if(and...)) system when I get proof by
contradiction working, which is almost identical to just using modus
ponens!

MP
t(R) <- if(L,R), t(L).

MP Variation
t(R) <- if(not(L),R), not(L).

t(R) <- if(not(R),L), not(L).

Herc

--
LOG20.PRO

PREDICATE CONSTRUCTION

if( and(X , Y ), or(X,Y) ).
if( and(not(X) , not(Y) ), not(or(X,Y)) ).
if( and(not(X) , Y ), or(X,Y) ).
if( and(X , not(Y) ), or(X,Y) ).

if( and(not(X) , not(Y) ), not(and(X,Y)) ).
if( and(not(X) , Y ), not(and(X,Y)) ).
if( and(X , not(Y) ), not(and(X,Y)) ).

if( and(X , Y ), if(X,Y) ).
if( and(not(X) , not(Y) ), if(X,Y) ).
if( and(not(X) , Y ), if(X,Y) ).
if( and(X , not(Y) ), not(if(X,Y)) ).

if( and(X , Y ), iff(X,Y) ).
if( and(not(X) , not(Y) ), iff(X,Y) ).
if( and(not(X) , Y ), not(iff(X,Y)) ).
if( and(X , not(Y) ), not(iff(X,Y)) ).

...

TRANSITIVE RULES...

if( and(if(A,B) , if(B,C)), if(A,C) ).

if( not(not(X)) , X ).
if( not(and(X,Y)) , or(not(X),not(Y)) ).
if( not(or(X,Y)) , and(not(X),not(Y)) ).

...

CARTESIAN JOIN OF THEOREMS

and(X,Y) :- t(X), t(Y).
and(X,not(Y)) :- t(X), not(Y).
and(not(X),not(Y)) :- not(X), not(Y).
and(not(X),Y) :- not(X), t(Y).

t(and(X,Y)) :- and(X,Y).

...

MODUS PONENS

t(R) :- if(L,R), t(L).

...

ARITHMETIC

t(less(X,Y)) :- less(X,Y).
less(0,X).
if( and(less(X,Y) , less(Y,Z)) , less(X,Z) ).

...

<NEXT WEEK IN FORMAL PROLOG - PROOF BY CONTRADICTION>

Date Subject Author
11/25/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Dan Christensen
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Graham Cooper
11/27/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Virgil
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/28/12 Graham Cooper
11/28/12 Dan Christensen
11/29/12 Graham Cooper
11/29/12 Dan Christensen
11/28/12 Frederick Williams
11/28/12 Dan Christensen
11/28/12 Dan Christensen