I was following these notes and I tried doing exercise (5) on page 42:
If $\varphi$ is an L-tautology, then $\vdash \varphi$ (without thm 2.7.4, completeness of predicate logic)
intuitively it makes sense (or it should be true) but I don't know how to even start a proof. Usually I would look at the list of axioms (propositional axioms, equality axioms, quantifier axioms) and try some of them. However, the equality axiom and quantifier axioms seem pretty useless because it feels really strange to introduce equality signs or quantifiers to a "virgin" L-tautology (which just is a formula of the form $p(\varphi_1, \dots, \varphi_n)$ for some tautology $p(\alpha_1, \dots, \alpha_n) \in Prop\{\alpha_1,\dots,\alpha_n \})$ i.e. introduce symbols to something that doesn't have them or doesn't need them.
Then I proceeded to check the propositional axioms since those seemed more plausible to be useful. The ones my notes provide as axioms are:
- T
- $\varphi \to (\varphi \lor \psi); \varphi \to (\psi \lor \varphi)$
- $\neg \varphi \to (\neg \psi \to \neg (\varphi \lor \psi) $
- $(\varphi \land \psi) \to \varphi; (\psi \land \varphi) \to \psi$
- $\varphi \to (\psi \to (\varphi \land \psi))$
- $(\varphi \to (\psi \to \theta)) \to ((\varphi \to \psi)\to (\varphi \to \theta))$
- $\varphi \to (\neg \varphi \to \bot)$
- $(\neg \varphi \to \bot) \to \varphi$
however, these propositional axioms already have formulas $\varphi,\psi,\theta$ and thus, it didn't seem sensible if I wanted to prove $p$ was a tautology, to introduce even more formulas...
Am I missing something really obvious? Or is this suppose to be hard?
-- For context, definition of Tautology
In propositional logic tautologies are those propositions $p$ that no matter the truth assignment to the atoms $t:A^n \to A$, $p$ is always true denoted $ \models p$. I assume that for predicate logic this definition is the same but with L-structures $\mathcal A = (A;(R^{\mathcal A})_{R \in L^r},(F^{\mathcal A})_{F \in L^f} )$ i.e. a L-formula $p(\varphi_1, \dots, \varphi_n)$ is a tautology if
$$\mathcal A \models p(\varphi_1, \dots, \varphi_n)$$
for all L-structures $\mathcal A$. I assume its denoted the same way $\models p(\varphi_1, \dots, \varphi_n)$ or $\models p$.
To give even more context I realized that I had a tautology and wanted to prove it from the axioms. Is:
$$ \varphi \to \exists x \varphi $$
which looks obviously true no matter what. Thus, I wanted to show that was true by using exercise (5) but (5) didn't depend on any specific tautology so that seemed odd to me.
Once I knew (5) I'd show that it is a tautology plugging in any L-structure and showing it always evaluates to True. Then invoke exercise (5).
A tautology is true in every structure, so $\models \varphi$. By the Completeness Theorem, $\vdash \varphi$.
(Here $\models \varphi$ and $\vdash \varphi$ are shorthand for $\emptyset\models \varphi$ and $\emptyset \vdash \varphi$, respectively.)
Edit (in response to a comment): The proof above uses Completeness for first-order logic. With just a little more care, you can prove this using only Completeness for propositional logic.
According to the definition in your notes, a tautology is a formula of the form $p(\varphi_1,\dots,\varphi_n)$, where $p(\alpha_1,\dots,\alpha_n)$ is a propositional tautology, and $\varphi_1,\dots,\varphi_n$ are first-order formulas. So $p(\varphi_1,\dots,\varphi_n)$ means that you substitute $\varphi_i$ for $\alpha_i$ in $p$, turning the propositional formula into a first-order formula.
Since $p(\alpha_1,\dots,\alpha_n)$ is a propositional tautology, there is a propoisitional proof of $p(\alpha_1,\dots,\alpha_n)$ (by Completeness for propositional logic). Now you can check that if you substitute the $\varphi_i$ for the $\alpha_i$ everywhere in the proof, you get a first-order proof of $p(\varphi_1,\dots,\varphi_n)$. This amounts to checking that every axiom and every application of a logical rule used in the propositional proof remains an axiom or a valid application of a logical rule in the first-order proof after substituting the $\varphi_i$ for the $\alpha_i$.