We introduce a formal proof system that will allow us to show that an [[Argument|argument]] is valid, when it is. The system, which is called $F_{r}$ (for **Fitch**), consists of a set of rules. We cannot use Fitch system gives schema of [[Logically Valid Argument|valid argument]] however it can't be used to show that an argument is invalid (we can only use counterexamples). A **[[Proof|proof]]** (in F) is a series of $L_{1}$ [[L1 (FOL)|sentences]], each of which is either a premise/assumption or derived from previous lines (and sub-proofs) according to rules. A proof is **a proof of** $\psi$ from $\varphi_{1},\dots,\varphi_{n}$ iff $\varphi_{1},\dots,\varphi_{n}$ are the premises of that proof and $\psi$ is the final line of it. Notation: ... For each connective, we have two rules: - An introduction rule which allows us to derive a sentence in which the relevant connective is the main connective (widest scope). - An elimination rule which allows us to derive something from a sentence in which the relevant connective is the main connective. Rules of inference : - Conjunction elimination ($\land \text{Elim}$): The rule says that if we have a sentence of the form $\varphi_{1} \land \varphi_{2}$ somewhere in the proof, we can derive $\varphi_{i}$, where $i = 1$ or $i=2$. - Conjunction Introduction ($\land \text{Intro}$): This rules says that we can derive $\varphi_{1} \land \varphi$, if somewhere in the proof we have $\varphi_{1}$ and also somewhere in the proof we have $\varphi_{2}$. - Disjunction Introduction ($\lor \text{Intro}$): This rule says that we can derive $\varphi_{1} \lor \varphi_{2}$, if we have $\varphi_{i}$ where $i=1$ or $i=2$, somewhere in the proof. The [[L1 (FOL)#^f198dd|contradiction]] (sentence that is false in every possible situation) symbol is $\perp$. It is syntactically treated as a sentence. - Contradiction Introduction ($\perp \text{Intro}$): If, somewhere in the proof, we have a sentence $\varphi$, and also, somewhere in the proof, we have the sentence $\lnot \varphi$, we can derive $\perp$. - Contradiction Elimination ($\perp \text{Elim}$): The rule says that if we have $\perp$ somewhere in the proof, we can derive any sentence. - Negation Elimination ($\lnot\text{Elim}$): The rule says that if we have a sentence of the form $\lnot \lnot \varphi$ somewhere in the proof, we can derive $\varphi$. - Negation Introduction ($\lnot \text{Intro}$): The rule says that if, somewhere in the proof, we have a **subproof** (proof inside the main proof) starting with $\varphi$ and ending with $\perp$, we can derive $\lnot \varphi$. NB: $\varphi$ is provable from no premises iff $(\vdash \varphi)$ is a [[L1 (FOL)#^e8f9c8|logical truth (tautology)]]. - Disjunction Elimination ($\lor \text{Elim}$): This rule says that if in the proof: (a) a sentence of the form $\varphi_{1} \lor \varphi_{2}$, (b) a subproof starting with $\varphi_{1}$ and ending with $\psi$ and (c) a subproof starting with $\varphi_{2}$ and ending with $\psi$, then we can derive $\psi$. - Reiteration ($\text{reit}$): The rule says we can derive $\varphi$. - Arrow Elimination ($\to \text{Elim}$): This rule is that if somewhere in the proof, we have $\varphi \to \psi$ and also somewhere in the proof, we have $\varphi$, we can derive $\psi$. - Arrow Introduction $(\to \text{Intro})$: The rule says that we can derive $\varphi \to \psi$, if, somewhere in the proof, we have a subproof which starts with $\varphi$ and ends with $\psi$. - Double arrow Elimination ($\leftrightarrow \text{Elim}$): The rule says that if we have a sentence of the form $\varphi \leftrightarrow \psi$ or $\psi \leftrightarrow \varphi$ and also somewhere in the proof we have $\varphi$ then we can derive $\psi$. - Double arrow Introduction ($\leftrightarrow \text{Intro}$): This rule says that if we can derive $\varphi \leftrightarrow \psi$ if we have a subproof that starts with $\varphi$ and ends with $\psi$, and also somewhere in the proof, a subproof that starts with $\psi$ and ends with $\varphi$.