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).