Rewriting First Order Logic

For all x such that phi :   (x) (phi)

Exist x:  [x]

Exist x such that phi :   [x] (phi)

Exist unique x such that phi:   [!x] (phi)

Exist many x such that phi:   [x..] (phi)

For all x e y. (phi):  (x) e y (phi)

Exist x e y. (phi):  [x] e y (phi)

Exist a/an object satisfying phi: [a/an phi]

For all objects satisfying Q: (Qs)

Exist a/an object in y, that satisfies phi: [a/an phi] e y

For all objects in y, satisfying Q: (Qs) e y

Sheffer stroke: |

Nor:  !

Exclusive Nor:  !!

Negation: ~

Conjunction: &

Disjunction: ?

Exclusive Disjunction: ??

Implication: ->

Converse Implication:  <-

Biconditional: <->

pi is a subformula of phi:  pi\phi

True: T

False: F

Proves: |-

Precedence brackets: ( )

Is defined as:  :=

Equality: =

Membership: e

Subset: c

Complement of x: x'

Union: U

Intersection: #

Exception: \

n_arity predicate phi: phi (x_1,...,x_n)

x has the relation R to y: x R y

n_arity function f: f(x_1,...,x_n)

function f from domain x to codomain y:  f:x-->y

Domain: dom

Range: rng

Ordered pair: <,>

Cartesian product of a and b:  a x b

Cardinality of x:  |x|

A class\set of x_1,...,x_n = {x_1,...,x_n}

A class\set of all phi objects: {x| phi}

Empty set: {} 

The class\set of all constructible sets: L

The class\set of all sets: V


Examples:

Extensionality: (x) (y) ((z) (z e x <-> z e y) -> x=y)

Regularity: [y] e x -> [y] e x (~[z] (z e x & z e y))

Empty:  [x] (y) (~ y e x)

Pairing: (a) (b) [{y| y=a ? y=b}]

Union: (a) [{y| [z] (y e z & z e a)}]

Power: (a) [{y| y c a}]

Infinity: [x] ({} e x & (y) e x (yU{y} e x))


Zuhair Al-Johar
Nov 21 2011
Nov 26 2011