Simple logic
| Paradigm(s) | Declarative |
|---|---|
| Designed by | User:Hakerh400 |
| Appeared in | 2023 |
| Computational class | Turing complete |
| Major implementations | Implemented |
| File extension(s) | .txt |
Simple logic is an esolang invented by User:Hakerh400 in 2023.
Overview
Simple logic is a very simple formal mathematical system of first-order logic and set theory. It has very basic inference rules, but it is powerful enough that we can implement Zermelo–Fraenkel set theory.
It has the following constants: zero succ var some set mem inp univ wff var_lt var_ne fresh subst
And the following inference rules:
var_zero_lt_succ :: set (var a) ⊢ var_lt zero (succ a) var_succ_lt_succ_of :: var_lt a b ⊢ var_lt (succ a) (succ b) var_ne_of_lt :: var_lt a b ⊢ var_ne a b fresh_var :: var_ne a b ⊢ fresh a (set (var b)) fresh_some_1 :: wff a, set (var b) ⊢ fresh b (some b a) fresh_some_2 :: wff a, set (var b), fresh c a ⊢ fresh c (some b a) fresh_mem :: set a, set b, fresh c a, fresh c b ⊢ fresh c (mem a b) fresh_imp :: wff a, wff b, fresh c a, fresh c b ⊢ fresh c (imp a b) fresh_univ_1 :: wff a, set (var b) ⊢ fresh b (univ b a) fresh_univ_2 :: wff a, set (var b), fresh c a ⊢ fresh c (univ b a) subst_var_1 :: set r, set (var x) ⊢ subst x r (var x) r subst_var_2 :: set r, var_ne x y ⊢ subst x r (var y) (var y) subst_some_1 :: set r, wff s, set (var x) ⊢ subst x r (some x s) (some x s) subst_some_2 :: wff s, var_ne x y, fresh y r, subst x r s a ⊢ subst x r (some y s) (some y a) subst_mem :: set s, set t, subst x r s a, subst x r t b ⊢ subst x r (mem s t) (mem a b) subst_imp :: wff s, wff t, subst x r s a, subst x r t b ⊢ subst x r (imp s t) (imp a b) subst_univ_1 :: set r, wff s, set (var x) ⊢ subst x r (univ x s) (univ x s) subst_univ_2 :: wff s, var_ne x y, fresh y r, subst x r s a ⊢ subst x r (univ y s) (univ y a) set_var_zero :: ⊢ set (var zero) set_var_succ :: set (var a) ⊢ set (var (succ a)) set_some :: set (var a)), wff b ⊢ set (some a b) wff_mem :: set a, set b ⊢ wff (mem a b) wff_imp :: wff a, wff b ⊢ wff (imp a b) wff_univ :: set (var a)), wff b ⊢ wff (univ a b) ax_imp_1 :: wff a, wff b ⊢ imp a (imp b a) ax_imp_2 :: wff a, wff b, wff c ⊢ imp (imp a (imp b c)) (imp (imp a b) (imp a c)) univ_i :: imp a b, fresh x a ⊢ imp a (univ x b) univ_e :: imp a (univ x b), subst x r b c ⊢ imp a c mp :: imp a b, a ⊢ b
On the left we have name of inference rule and on the right we have inference scheme. The identifiers in blue can be substituted with any expression.
Inference rules are separated into three groups (for readability). The first group represents technical rules (regarding variable substitution). The second group defines how expressions (sets and wffs) can be built. The third group represents the actual axioms and inference rules of logic.
Note that zero and succ do not represent natural numbers in the set-theoretic way. They are just technical terms used here to specify set variables (variable "a" can be represented as zero, variable "b" as succ zero, and so on).
Definitions
As we can see, the only logical connective we have is implication imp and the only quantifier is the universal quantifier univ. But that is actually everything we need. We can model the rest of logic using only those two.
False can be defined as ⊥ := ∀ a b, a ∈ b. In technical terms that would be univ zero (univ (succ zero) (mem (var zero) (var (succ zero)))). We can use inference rules to prove that this is indeed a wff.
True can be defined as ⊤ := ⊥ → ⊥
Negation can be defined as ¬P := P → ⊥
Disjunction P ∨ Q := ¬P → Q
Conjunction P ∧ Q := ¬(¬P ∨ ¬Q)
Equivalence P ↔ Q := (P → Q) ∧ (Q → P)
Existential quantifier ∃ x, P := ¬∀ x, ¬P
Proofs
Just like constructing expressions, we can use inference rules to prove propositions. See the reference implementation to see how we proved ⊢ ⊤ (true holds).
Note that constructing a proposition and proving a proposition are two very different things. We can construct any syntactically valid proposition, even if the proposion itself is false. For instance, we can easily prove ⊢ wff ⊤, but proving ⊢ ⊤ is much more difficult. Also, we can prove ⊢ wff ⊥, but we cannot prove ⊢ ⊥.