Philosophy of Abstraction Logic

Introduction

What is Logic?

Calculator Logic

Values, Operations, Operators

Abstraction and Shape

• The arity $n$ is zero (which implies $m = 0$, because we excluded degenerate shapes) and $o$ is a value.
• The valence $m$ is zero, the arity $n$ is non-zero, and $o$ is an $n$-ary operation. Note that $o$ is then necessarily a proper operation.
• The valence $m$ is non-zero (which implies $n > 0$) and $o$ is an $n$-ary operator, such that $o$ accepts in argument position $i$ a ${|{p_i}|}$-ary operation. Here ${|{p_i}|}$ is the size of $p_i$. Note that $o$ is then necessarily a proper operator.

Syntax

Logic

• The abstraction $\top$, intended to denote a value.
• The abstraction $⇒$, intended to denote a binary operation.
• The abstraction $\forall$, intended to denote a proper unary operator.

Several Abstraction Logics

1. $⊤$
2. $A ⇒ (B ⇒ A)$
3. $(A ⇒ (B ⇒ C)) ⇒ ((A ⇒ B) ⇒ (A ⇒ C))$
4. $(∀ x.\,A[x]) ⇒ A[x]$
5. $(∀ x.\,A ⇒ B[x]) ⇒ (A ⇒ (∀ x.\, B[x]))$

6. $x = x$
7. $x = y ⇒ (A[x] ⇒ A[y])$
8. $A ⇒ (A = ⊤)$

9. $⊥ = (∀ x.\, x)$
10. $¬ A = (A ⇒ ⊥)$
11. $(x ≠ y) = ¬(x = y)$

12. $(A ∧ B) ⇒ A$
13. $(A ∧ B) ⇒ B$
14. $A ⇒ (B ⇒ (A ∧ B))$
15. $A ⇒ (A ∨ B)$
16. $B ⇒ (A ∨ B)$
17. $(A ∨ B) ⇒ ((A ⇒ C) ⇒ ((B ⇒ C) ⇒ C))$
18. $(A \Leftrightarrow B) = ((A ⇒ B) ∧ (B ⇒ A))$
19. $A[x] ⇒ (∃ x.\, A[x])$
20. $(∃ x.\, A[x]) ⇒ ((∀ x.\, A[x] ⇒ B) ⇒ B)$

21. $A ∨ ¬ A$

Calculator Logic as an AL

Primitive Abstractions

Definitions

Literals

Axioms

• $(\operatorname{right-neutral}\, x\, y.\, (x + y)\, 0)$
• $(\operatorname{right-neutral}\, x\, y.\, (x \times y)\, 1)$
• $(\operatorname{closed}\,x\,y.\, (\text{Num}.\, x)\, (x + y))$
• $(\operatorname{closed}\,x\,y.\, (\text{Num}.\, x)\, (x \times y))$
• $(\operatorname{closed}\,x.\, (\text{Num}.\, x)\, (- x))$
• $(\operatorname{comm}\, x\, y.\, x + y)$
• $(\operatorname{assoc}\, x\, y.\, x + y)$
• $(\operatorname{comm}\, x\, y.\, x \times y)$
• $(\operatorname{assoc}\, x\, y.\, x \times y)$
• $(\operatorname{distr}\, x\, y.\, (x + y)\, (x \times y))$
• $(\text{Num}.\, x\, y) ⇒ x - y = x + (-y)$
• $(\text{Num}.\, x\,y\, z)⇒ y ≠ 0 ⇒ (x \div y = z) = (x = z \times y)$
• $(\text{Num}.\, x) ⇒ x - x = 0$
• $(\text{Num}.\, x\,y\, z) ⇒ z ≠ 0 ⇒ z \times x = z \times y ⇒ x = y$
• $(\operatorname{closed}\,x\,y.\, (\text{Pos}.\, x)\, (x + y))$
• $(\operatorname{closed}\,x\,y.\, (\text{Pos}.\, x)\, (x \times y))$
• $(\text{Num}.\, x) ⇒ (\text{either-or}.\, (\text{Pos}.\, x)\, (x = 0)\, (\text{Pos}.\, {-x}))$
• $A[1] ⇒ (\forall x.\, A[x] ⇒ A[x + 1]) ⇒ (\text{Pos}.\, x) ⇒ A[x]$

Undefinedness

• Abstraction “$\Finv$” is added, denoting a value.
• $(\operatorname{domain-bound} x.\, D[x]\, F[x]) ≝ (\forall x.\, ¬ D[x] ⇒ F[x] = \Finv)$
• $(\operatorname{domain-bound} x\, y.\, D[x]\, F[x, y]) ≝ (\forall x\, y.\, ¬ (D[x] ∧ D[y]) ⇒ F[x, y] = \Finv)$
• $(\exists_1 x.\, A[x]) ≝ (∃ x.\, A[x] ∧ (\forall y.\, A[y] ⇒ x = y))$
• Abstraction “$\operatorname{the}$” is added, denoting a proper unary operator.
• $(\exists_1 x.\, A[x]) ⇒ A[x] ⇒ (\operatorname{the} x.\, A[x]) = x$
• $¬ (\exists_1 x.\, A[x]) ⇒ (\operatorname{the} x.\, A[x]) = \Finv$

• $(\text{either-or}.\ ((x = \top) ∨ (x = \bot))\, (\text{Num}.\, x) \,(x = \Finv))$
• $(\operatorname{domain-bound} x\, y.\, (\text{Num}.\, x)\, (x + y))$
• $(\operatorname{domain-bound} x.\, (\text{Num}.\, x)\, (- x))$
• $(\operatorname{domain-bound} x\, y.\, (\text{Num}.\, x)\, (x \times y))$
• We drop the previous axiom governing division.
• $x \div y = (\operatorname{the} z.\, (x = z \times y))$

[...] it is very unusual in mathematical practice to use truth values beyond true and false. Moreover, the presence of a third truth value makes the logic more complicated to use and implement.

Semantics

• If $t = x$ where $x$ is a variable, then $\llbracket t \rrbracket = \nu(x, 0)$.
• If $t = x[t_0, \ldots, t_{n-1}]$ is a variable application with $n > 0$, then $$\llbracket t \rrbracket = f(u_0, \ldots, u_{n-1})$$ where $f = \nu(x, n)$ is the $n$-ary operation assigned to $x$ via the valuation $\nu$, and $u_i$ is the value of $t_i$ with respect to $\nu$.
• If $t = (a.)$ then $\llbracket t \rrbracket = u$, where $a$ denotes the value $u$.
• If $t = (a.\, t_0 \ldots t_{n-1})$ for $n > 0$, then $$\llbracket t \rrbracket = f(u_0, \ldots, u_{n-1})$$ where $a$ denotes the $n$-ary operation $f$, and $u_i$ is the value of $t_i$ with respect to $\nu$.
• Assume $t = (a\, x_0\ldots x_{m-1}.\, t_0 \ldots t_{n-1})$ for $m > 0$, and let the shape of $a$ be $(m; p_0, \ldots, p_{n-1})$. Let $F$ be the $n$-ary operator denoted by $a$. We define the arguments $r_i$ to which we will apply $F$ as follows. If $p_i = \emptyset$, then $r_i$ is the value denoted by $t_i$ with respect to $\nu$. If $p_i = \{j_0, \ldots, j_{k-1}\}$ for ${|{p_i}|} = k > 0$, then the abstraction $a$ binds the variables $x_{j_0}, \ldots, x_{j_{k-1}}$ occurring with arity $0$ in $t_i$. Thus $r_i$ is the $k$-ary operation which maps $k$ values $u_0, \ldots, u_{k-1}$ to the value denoted by $t_i$ with respect to the valuation $\nu[x_{j_0} \coloneqq u_0, \ldots, x_{j_{k-1}} \coloneqq u_{k-1}]$. Then $$\llbracket t \rrbracket = F(r_0, \ldots, r_{n-1})$$

Substitution

Substitution as Valuation

• If $n = 0$, then $\nu_\sigma(x, n) = \llbracket {{x} / {\sigma}} \rrbracket$.
• If $n > 0$, then for any values $u_0, \ldots, u_{n-1}$ we define $$\nu_\sigma(x, n)(u_0, \ldots, u_{n-1}) = \llbracket {t} \rrbracket_{y \coloneqq u}$$ where $\sigma(x, n) = [y_0 \ldots y_{n-1}.\, t]$, and $\llbracket {\cdot} \rrbracket_{y \coloneqq u}$ evaluates with respect to the valuation $\nu[y_0 \coloneqq u_0, \ldots, y_{n-1} \coloneqq u_{n-1}]$.

Models

1. We are not interested in all possible abstraction algebras as models, but only in those that are logic algebras.
2. We are not interested in testing the axioms with all possible valuations, but only with those that belong to a space of valuations depending on the model itself.

• $I(⇒)(I(\top), u) = I(\top)$ implies $u = I(\top)$ for all values $u$ in $\mathcal{U}$.
• Let $f$ be any unary operation of $\mathcal{U}$ such that $f(u) = I(\top)$ for all values $u$ in $\mathcal{U}$. Then $I(\forall)(f) = I(\top)$.

• $\mathcal{V}$ is not empty.
• If $\nu$ is a valuation belonging to $\mathcal{V}$, $u$ is a value in the universe of ${\mathfrak{A}}$, and $x$ is a variable in $X$, then $\nu[x \coloneqq u]$ also belongs to $\mathcal{V}$.
• If $\nu$ is a valuation belonging to $\mathcal{V}$, and if $\sigma$ is a substitution with respect to the signature of ${\mathfrak{A}}$, then $\nu_\sigma$ also belongs to $\mathcal{V}$.

Proofs

1. An axiom invocation $\operatorname{AX}(t)$ such that $t$ is an axiom in ${\mathbb{A}}$.
2. An application of substitution $\operatorname{SUBST}(t, \sigma, p_s)$ where
   • $p_s$ is proof of $s$ in ${\mathcal{L}}$
   • $\sigma$ is a substitution
   • $t$ and ${s} / {\sigma}$ are $\alpha$-equivalent
3. An application of modus ponens $\operatorname{MP}(t, p_h, p_g)$ such that
   • $p_h$ is a proof of $h$ in ${\mathcal{L}}$
   • $p_g$ is a proof of $g$ in ${\mathcal{L}}$
   • $g$ is identical to $h ⇒ t$
4. Introduction of the universal quantifier $\operatorname{ALL}(t, x, p_s)$ where
   • $x$ is a variable
   • $p_s$ is a proof of $s$ in ${\mathcal{L}}$
   • $t$ is identical to $(\forall x.\, s)$

The Deduction Theorem

Soundness

• Assume $p = \operatorname{AX}(t)$. Then $t$ is an axiom and is therefore valid.
• Assume $p = \operatorname{SUBST}(t, \sigma, p_s)$. Then $p_s$ is a proof of $s$, and therefore $s$ is valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Then $$\llbracket t \rrbracket = \llbracket {s / {\sigma}} \rrbracket = {\llbracket s \rrbracket}_\sigma$$ Because $\nu_\sigma$ is in $\mathcal{V}$ as well, and $s$ is valid, $${\llbracket s \rrbracket}_\sigma = I(⊤)$$ Together this yields $\llbracket t \rrbracket = {\llbracket s \rrbracket}_\sigma = I(⊤)$.
• Assume $p = \operatorname{MP}(t, p_h, p_g)$. Then $p_h$ is a proof of $h$, and $p_g$ is a proof of $g$, and therefore both $h$ and $g$ are valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Then $\llbracket h \rrbracket = I(⊤)$ and $$I(⊤) = \llbracket g \rrbracket = \llbracket {h ⇒ t} \rrbracket = I(\text{⇒})(\llbracket h \rrbracket, \llbracket t \rrbracket) = I(\text{⇒})(I(⊤), \llbracket t \rrbracket)$$ This implies $\llbracket t \rrbracket = I(⊤)$.
• Assume $p = \operatorname{ALL}(t, x, p_s)$. Then $p_s$ is a proof of $s$, and therefore $s$ is valid. Let $\nu$ be a valuation in $\mathcal{V}$ for some model $({\mathfrak{A}}, \mathcal{V})$ of ${\mathcal{L}}$. Let $\mathcal{U}$ be the universe of ${\mathfrak{A}}$. Then $$\llbracket t \rrbracket = \llbracket {(\text{∀} x.\, s)} \rrbracket = I(\text{∀})(f)$$ Here $f$ is a unary operation of $\mathcal{U}$ where $f(u) = {\llbracket s \rrbracket}_{x \coloneqq u}$ for all values $u$ in $\mathcal{U}$. Because $\nu[x \coloneqq u]$ also belongs to $\mathcal{V}$ and $s$ is valid, we have ${\llbracket s \rrbracket}_{x \coloneqq u} = I(⊤)$ and therefore $f(u) = I(⊤)$ for all $u$. This implies $\llbracket t \rrbracket = I(\text{∀})(f) = I(⊤)$.