First Order Logic

Chenkai Wang

0. Introduction

Mathematics is all about logic. Every insightful mathematical theory (among non-mathematical ones) is built up by certain kinds of rules (axiomatically). The rules which enable us to produce a theory system are introduced by formal theory. Don't mix formal theory with the actual theory you are playing with! We sometimes call formal theory a metatheory. The study of formal theory falls into the realm of mathematical logic, which is the novel frontier of the study of logic from the late 18th century until nowadays. The philosophical inception such as the relating ontology was investigated by true logicians which will not be covered here. Among all different formal systems, first order theories are the most useful one. OK, we now onto the main subject: first order logic.

1. The Language

We call our first order logic a language because it simulates our natural language, but it's more accurate. The main difference between a natural language and a formal language is our formal languages can never have ambiguity. You can never have one thing representing two different other things based on your context. (However, in our informal discussion, we usually omit this rule when the ambiguity can be easily dropped for convenience, but it is still better than our natural languages.)

A first order theory MUST consists all of the followings:

1. some constant symbols
2. some object variable symbols
3. some well-formed formula (wff) variable symbols

1-3 are called alphabet or just symbols, you can define new type of alphabet later on, but that's not primitive. 1-3 are not inter-definable.

4. some rules which acts on constants and object variables for constructing well-formed formula
5. some axioms, must be well-formed formulas
6. some inference rules which acts on well-formed formulas for constructing new well-formed formulas from axioms

4-6 are called syntax or rules of our first order language. Please note that axioms can be defined as inference rules just producing crisp new well-formed formulas from no previous ones. We state the axiom here because of its importance and convenience. 4 and 6 are not inter-definable.

OK on to these building blocks themselves:
1. $ \quad \lnot,\,\rightarrow,\,\forall $
2. $ \quad x,\,y,\,z,\,\cdots $
3. $ \quad \varphi,\,\psi,\,\chi,\,\cdots $

\documentclass[10pt,letterpaper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry}
\author{Chenkai Wang}
\title{First Order Logic}
\begin{document}
\maketitle
\section{Introduction}
Mathematics is all about logic. Every insightful mathematical theory (among non-mathematical ones) is built up by certain kinds of rules (axiomatically). The rules which enable us to produce a theory system are introduced by formal theory. Don't mix formal theory with the actual theory you are playing about! We sometimes call formal theory a metatheory. The study of formal theory falls into the realm of mathematical logic, which is the novel frontier of the study of logic from the late 18th century until nowadays. The philosophical inception such as the relating ontology was investigated by true logicians which will not be covered here. Among all different formal systems, first order theories are the most useful one. OK, we now onto the main subject: first order logic.
\section{The Language}
We call our first order logic a language because it simulates our natural language, but it's more accurate. The main difference between a natural language and a formal language is our formal languages can never have ambiguity. You can never have one thing representing two different other things based on your context. (However, in our informal discussion, we usually omit this rule when the ambiguity can be easily dropped for convenience, but it is still better than our natural languages.)\\
\\
A first order theory MUST consists all of the followings:\\
\\
1. some constant symbols\\
2. some object variable symbols\\
3. some well-formed formula (wff) variable symbols\\
\\
1-3 are called alphabet or just symbols, you can define new type of alphabet later on, but that's not primitive. 1-3 are not inter-definable.\\
\\
4. some rules which acts on constants and object variables for constructing well-formed formula\\
5. some axioms, must be well-formed formulas\\
6. some inference rules which acts on well-formed formulas for constructing new well-formed formulas from axioms\\
\\
4-6 are called syntax or rules of our first order language. Please note that axioms can be defined as inference rules just producing crisp new well-formed formulas from no previous ones. We state the axiom here because of its importance and convenience. 4 and 6 are not inter-definable.
\end{document}

2. Some Useful Metatheorems

1. Deduction Theorem

3. miscellanea

"SUCH THAT" is confusing!