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