|
|
Re: PREDICATE CALCULUS 2
Posted:
Nov 27, 2012 9:38 AM
|
|
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
Download my DC Proof 2.0 software at http://www.dcproof.com
|
|
