|
|
|
Viewing Version
1
of
'first order logic'
|
[ view 'first order logic'
|
back to history
]
| Title of object: |
first order logic |
| Canonical Name: |
FirstOrderLogic |
| Type: |
Definition |
| Created on: |
2002-08-28 22:11:13.068784-04 |
| Modified on: |
2002-08-28 22:11:13.068784-04 |
| Classification: |
msc:03B10 |
| Synonyms: |
first order logic=classical first order logic
first order logic=FO |
Revision comment (for changes between this and next version):
| Changes for correction #1034 ('lists for readability'). |
Preamble:
% this is the default PlanetMath preamble. as your knowledge
% of TeX increases, you will probably want to edit this, but
% it should be fine as is for beginners.
% almost certainly you want these
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
% used for TeXing text within eps files
%\usepackage{psfrag}
% need this for including graphics (\includegraphics)
%\usepackage{graphicx}
% for neatly defining theorems and propositions
%\usepackage{amsthm}
% making logically defined graphics
%\usepackage{xypic}
% there are many more packages, add them here as you need them
% define commands here
%\PMlinkescapeword{theory} |
Content:
A logic is \emph{first order} if it has exactly one type. Usually the term refers specifically to the logic with connectives $\neg$, $\vee$, $\wedge$, $\rightarrow$, and $\leftrightarrow$ and the quantifiers $\forall$ and $\exists$, all given the usual semantics:
$\neg\phi$ is true iff $\phi$ is not true
$\phi\vee\psi$ is true if either $\phi$ is true or $\psi$ is true
$\forall x\phi(x)$ is true iff $\phi^t_x$ is true for every object $t$ (where $\phi^t_x$ is the result of replacing every unbound occurance of $x$ in $\phi$ with $t$)
and the others are defined by:
$\phi\wedge\psi$ is the same as $\neg(\neg\phi\vee\neg\psi)$
$\phi\rightarrow\psi$ is the same as $(\neg\phi)\vee\psi$
$\phi\leftrightarrow\psi$ is the same as $(\phi\rightarrow\psi)\wedge(\psi\rightarrow\phi)$
$\exists x\phi(x)$ is the same as $\neg\forall x\neg\phi(x)$
However languages with slightly different quantifiers and connectives are sometimes still called first order as long as there is only one type. |
|
|
|
|
|
