Induction over propositional formulas

Question

The very first thing one usually does in a logic course is to defines a formal language for the propositional logic.

I don't want to bother what a "logic" is and why we need a "language" which we define know for a "logic".

A language consists of an ALPHABET and a GRAMMAR.

An alphabet $\mathcal{A}$ is a union of three different sets, we will call the element of an alphabet symbols. The first set are the symbols for the propositional variables like $A,B,C....$, the second set is the set of logical symbols $T,F,\wedge,\vee,\implies,\iff$ and the thirs set are non-logical symbols like $(,)$

Now here comes the first thing I don't understand yet we say a propositional formula is a sequence of symbols that satisfies certain rules. What I don't understand is how exactly I can write the set I take an element from when I say: Assume $\phi$ is a propositional formula. Maybe somebody can help me.

The condition that has to be satisfied if $\phi$ wants to be an element of the set of all statements (that I don't know how to define in logical notation) are: $\phi$ is a propositional variable($\iff \phi$ is a function with domain $\{1\}$ and range $\mathcal{A}$ and $\phi(1)$ is a propositional variable) or $\phi$ is $F$( $\iff \phi$ is a function with domain $\{1\}$ and range $\mathcal{A}$ and $\phi(1)=F$) or $\phi$ is $T$ ( $\iff \phi$ is a function with domain $\{1\}$ and range $\mathcal{A}$ and $\phi(1)=T$) or there is a $ n\in\mathbb{N}$ such that $n\geq 2$ and $\phi$ is a function with domain $\{1,...,n\}$ and range $\mathcal{A}$ and $\phi(1)=\neg$ and $\psi:\{1,...,n-1\}\rightarrow \mathcal{A}$ with $\forall k\in\{1,...,n-1\}\psi(k)=\phi(k+1)$ is a propositional formula or there is a $n\in\mathbb{N}$ and a $k\in\mathbb{N}$ such that $n\geq 5$ and $k\in\{2,...,n-1\}$ and $\phi$ is a function with domain $\{1,...,n\}$ and range $\mathcal{A}$ and $\phi(1)=($ and $\phi(n)=)$ and $\phi(k)=\wedge\backslash\vee\backslash\implies\backslash\iff$ and $\psi_1:\{1,....,k-2\}\rightarrow \mathcal\{A\}$ with $\forall j\in{1,...,k-2}\psi_1(j)=\phi(j+1)$ and $\psi_2:\{1,...,(n-1)-k\}$ with $\forall z\in \{1,...,(n-1)-k\}\psi_2(z)=\phi(z+k)$ are propositional formulas.

My question to you how can I prove this claim:

If a property holds for every constant (propositional variable,T,F) and the implications ( $a$ is a propositional formula and $a$ has property $\Rightarrow \neg a$ has property,$a$ and $b$ are propostioanl formulas and $a$ and $b$ have property then $a\wedge b$ has property (and so on for the other logical operationsyymbols)) are true then every propositional formula has the property.

I am trying to find a way to prove this by induction over the natural numbers $n\in\mathbb{N}$, however I didn't succeed in building this bridge. I was reading a book (H.-D Ebbinghaus,J.Flum,W.Thomas) and they have proposed to define the notion of a derivation with a lenght $n\in\mathbb{N}$ and then show that the claim above implies that every derivation fullfils the property. Which then in turn means every element fullfills the property because every element has (or is) a derivation.

An example of what a derivation is

$((A\wedge B)\vee C) $ is a propositional formula because there exists a derivation, namely

1. $C$ is a propositional constant

2. $A$ is a propositional constant

3. $B$ is a propositional constant

4. $(A\wedge B)$ is a propositional formula because of $3.$ and $2.$

5. $((A\wedge B)\vee C)$ is a propositional formula because of $4.$ and $1.$ This derivation has a length of $5$

I have tried to define what a derivation is and to prove that every propositional formula has (or is[because it depends on how we define derivation]) a derivation.

I came to an unsatisfying result. Because I didn't see another way to prove that every propositional formula has a derivation other than changing the definition of what a propositional formula itself is. Thus I have first defined what a derivation is and then said what a propositional formula is, namely objects that we get from certain derivations (the derivation itself depends on "rules" thats why I said certain here). This however prompted a new problem. Namely that if I go the other way around and already have an element I cannot use the prior convenient definition anymore and because the definition that I came up with didn't match the definition which the author intended, I couldn't understand the following proofs in the book anymore. I hope somebody can help me to find a a way to define what a derivation is and then to prove that every propositional has a derivation and eventually to prove the claim above by using this definition of a derivation. My only goal is to find a proof for the claim which preserves the definition of a propositional formula. The above paragraph was just a proposal and described my efforts and thinking-process so far.

If you want to know more details about the work I have done so far please tell me I will edit then, and thank you for reading this long text.

Answer 1

The most convenient approach is to stop talking about sequences of characters. Ideally, you would simply define a formula to be a tree-like structure upon which you could directly do (structural) induction. Here's one formal, set-theoretic way to describe it:

Write $\mathcal F$ for the set of formulas and $V$ for a set of proposition variables. For simplicity, I'll assume that only $\bot$ and $\to$ are connectives, but the pattern should be clear to include others. It is define as the smallest set which is closed under the connectives. Specifically, $0\in\mathcal F$, $v\in V$ implies $(1,v)\in\mathcal F$, and $\varphi,\psi\in\mathcal F$ implies $(2,\varphi,\psi)\in\mathcal F$. We can then use $\bot$ as notation for $0$, $v$ as (ambiguous) notation for $(1,v)$, and $\varphi\to\psi$ for $(2,\varphi,\psi)$¹. Furthermore, for all sets $X$ satisfying the same constraints (with $X$ in the place of $\mathcal F$), $\mathcal F\subseteq X$. If you unfold this last statement, you find it is exactly a structural induction rule for $\mathcal F$ that looks like $$\dfrac{0\in X\qquad \forall v\in V.(1,v)\in X\qquad \forall \varphi,\psi\in X.(2,\varphi,\psi)\in X}{\forall \varphi\in\mathcal F.\varphi\in X}$$ In particular, choosing $X=\{\varphi\in\mathcal F\mid P(\varphi)\}$ we have $X=\mathcal F$ (i.e. $\forall \varphi\in\mathcal F.P(\varphi)$) if and only if $P(0)$, $\forall v\in V.P((1,v))$, and $\forall \varphi,\psi\in\mathcal F.P(\varphi)\land P(\psi)\implies P((2,\varphi,\psi))$. Your question with formulas defined as above is just to do the unfolding I described and see that this is so.

Starting from sequences of characters, the difficult part is recovering this tree. This depends on how the syntax of formulas is described to you. This is a problem of formal language theory and is completely independent of logic in that it is the same problem for arithmetic expressions or programming language source code. Most likely, if you are not using a variation of Polish notation, the language is described in a way that can be formalized using a context-free grammar.² The theory of context-free grammars will give you a notion of a concrete syntax tree which you can then define a structurally recursive function over to simplify it to the form of the previous paragraph which can be considered an abstract syntax tree. Or you could combine these steps together. You would want to show that this process produces a unique abstract syntax tree for every source sequence of characters (probably primarily by showing the context-free grammar is deterministic) and that every abstract syntax tree (i.e. element of $\mathcal F$) can be represented by some sequence of characters.

What might be easiest approach to this without introducing a bunch of machinery is to use the inductive definition of $\mathcal F$ to define a function $f:\mathcal F\to\mathbf{2}^{\Sigma^*}$ where $\Sigma$ is the alphabet and so $\Sigma^*$ is the set of sequences of characters in that alphabet. In other words, this function produces sets of sequences of characters. This function would take an abstract syntax tree and produce the set of all sequences of characters that correspond to it. You would want to prove that the output of this function was never empty and each output was disjoint from every other output. This produces $\mathcal L = \bigcup_{\varphi\in\mathcal F}f(\varphi)$ and a function $g:\mathcal L\to\mathcal F$ satisfying $g^{-1}(\varphi)=f(\varphi)$ which allows us to transport the inductive structure of $\mathcal F$ to $\mathcal L$. In particular, we get $$\dfrac{\forall s\in f(0).s\in Y\qquad \forall v\in V.\forall s\in f((1,v)).s\in Y\qquad \forall s_1,s_2\in Y.\forall s\in f((2,s_1,s_2)).s\in Y}{\forall s\in\mathcal L.s\in Y}$$ This is accomplished essentially by defining $\varphi\in X\iff \forall s\in\mathcal L.g(s)=\varphi \implies s\in Y$ and using this in the earlier structural induction rule. Another perspective on this is $\{f(\varphi)\mid \varphi\in\mathcal F\}$ partitions $\mathcal L$, so we can view formulas as representing equivalence classes of sequences of characters in the language. This set of equivalence classes is in bijection with $\mathcal F$. We can then talk in terms of representative sequences of characters assuming we have $y\in Y\land y\sim y'\implies y'\in Y$ where $\sim$ is the equivalence relation induced by the partitioning. Given this constraint on $Y$, we could write things like $$\dfrac{``\bot"\in Y\qquad \forall v\in V.\mathsf{var}(v)\in Y\qquad \forall \varphi,\psi\in Y.\varphi\frown``\to"\frown\psi\in Y}{\forall \varphi\in\mathcal L.\varphi\in Y}$$ where $\mathsf{var}(v)$ produces a sequence of characters that corresponds to $v$ and $\frown$ is concatenation of sequences of characters. The idea being that ${``{A\to B}"} \sim {``{(A\to B)}"}$.

¹ What's really happening here is an explicit construction of a disjoint union, like $\{\varnothing\}\uplus V \uplus \mathcal F\times\mathcal F$. More connectives would lead to more summands in this disjoint union.

² (Reverse) Polish notation could also be described via a context-free grammar, but is simple and regular enough that you can also directly prove theorems about it by structural induction on sequences of characters.

Answer 2

It's easy to prove this by induction on the natural numbers. Say the "length" of a formula is the number of characters, and prove $P(n)$ by induction on $n$, where $P(n)$ is the statement that every formula of length less than or equal to $n$ has the property.