====
Variable
====

x
var_name_1_

---

(proof (block
  (expression (variable))
  (expression (variable))))


====
Function
====

A(x)
B
A(E x . P(x))
T(x)
F(x)

---

(proof (block
  (expression (function (function_name) (variable)))
  (expression (function (function_name)))
  (expression
    (function
      (function_name)
      (exists
        (variable)
        (function (function_name) (variable)))))
  (expression (function (function_name) (variable)))
  (expression (function (function_name) (variable)))))


====
True & False
====

T
1
⊤
F
0
⊥

---

(proof (block
  (expression (true))
  (expression (true))
  (expression (true))
  (expression (false))
  (expression (false))
  (expression (false))))


====
Not
====

-x
!x
~x
¬x
--x

---

(proof (block
  (expression (not (variable)))
  (expression (not (variable)))
  (expression (not (variable)))
  (expression (not (variable)))
  (expression (not (not (variable))))))


====
And
====

x ^ y
x & y
x ∧ y

---

(proof (block
  (expression (and (variable) (variable)))
  (expression (and (variable) (variable)))
  (expression (and (variable) (variable)))))


====
Or
====

x _ y
x | y
x v y
x ∨ y

---

(proof (block
  (expression (or (variable) (variable)))
  (expression (or (variable) (variable)))
  (expression (or (variable) (variable)))
  (expression (or (variable) (variable)))))


====
Implies
====

x -> y
x => y
x → y
x ⇒ y

---

(proof (block
  (expression (implies (variable) (variable)))
  (expression (implies (variable) (variable)))
  (expression (implies (variable) (variable)))
  (expression (implies (variable) (variable)))))


====
Iff
====

x <-> y
x <=> y
x ↔ y
x ⇔ y
x ≡ y

---

(proof (block
  (expression (iff (variable) (variable)))
  (expression (iff (variable) (variable)))
  (expression (iff (variable) (variable)))
  (expression (iff (variable) (variable)))
  (expression (iff (variable) (variable)))))


====
Forall
====

A x . A(x)
∀ x . x

---

(proof (block
  (expression
    (forall
      (variable)
      (function (function_name) (variable))))
  (expression (forall (variable) (variable)))))


====
Exists
====

E x . E(x)
∃ x . x

---

(proof (block
  (expression
    (exists
      (variable)
      (function (function_name) (variable))))
  (expression (exists (variable) (variable)))))