%2multibyte Version: 5.50.0.2890 CodePage: 1253

\documentclass{article}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\usepackage{amssymb}
\usepackage{amsmath}

\setcounter{MaxMatrixCols}{10}
%TCIDATA{OutputFilter=LATEX.DLL}
%TCIDATA{Version=5.50.0.2890}
%TCIDATA{Codepage=1253}
%TCIDATA{<META NAME="SaveForMode" CONTENT="1">}
%TCIDATA{BibliographyScheme=Manual}
%TCIDATA{Created=Sunday, April 17, 2011 01:30:07}
%TCIDATA{LastRevised=Wednesday, July 06, 2011 03:12:49}
%TCIDATA{<META NAME="GraphicsSave" CONTENT="32">}
%TCIDATA{<META NAME="DocumentShell" CONTENT="Standard LaTeX\Blank - Standard LaTeX Article">}
%TCIDATA{CSTFile=40 LaTeX article.cst}

\newtheorem{theorem}{Theorem}
\newtheorem{acknowledgement}[theorem]{Acknowledgement}
\newtheorem{algorithm}[theorem]{Algorithm}
\newtheorem{axiom}[theorem]{Axiom}
\newtheorem{case}[theorem]{Case}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{conclusion}[theorem]{Conclusion}
\newtheorem{condition}[theorem]{Condition}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{criterion}[theorem]{Criterion}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{solution}[theorem]{Solution}
\newtheorem{summary}[theorem]{Summary}
\newenvironment{proof}[1][Proof]{\noindent \textbf{#1.} }{\  \rule{0.5em}{0.5em}}
\input{tcilatex}
\begin{document}


\begin{equation*}
\text{\textbf{Stratified Models in First-Order Logic}}
\end{equation*}%
\begin{equation*}
\text{Jos\'{e} Roquette}
\end{equation*}%
\begin{equation*}
\text{\textit{Departamento de Matem\'{a}tica}}
\end{equation*}%
\begin{equation*}
\text{\textit{Instituto Superior T\'{e}cnico, Lisbon, Portugal}}
\end{equation*}%
\begin{equation*}
\mathit{jroquet@math.ist.utl.pt}
\end{equation*}%
\begin{equation*}
\text{\textbf{Abstract}}
\end{equation*}

We introduce \textit{stratification} in first-order logic; then we discuss 
\textit{soundness}, \textit{conservativeness} and \textit{completeness.}

\bigskip

\textbf{0. Introduction.}

The various nature of the mathematical objects in what concerns their
complexity, our knowledge of them or the possibility to make them explicit
(for ex\nolinebreak ample, infinitesimal or ilimited real numbers) is a
strong motivation to consider their distribution into \textit{levels }or%
\textit{\ strata. }The \textit{stratification }depends on the selected
property (or properties) of the mathematical objects that are the subject-%
\newline
-matter of our study.

\bigskip

\textbf{1. Stratified Models.}

Along this article $\mathcal{L}$ is a first-order language with equality, no
constant symbols, no function symbols and the logical symbols:

\textit{parentheses} \  \ $\  \  \  \  \  \  \  \  \  \  \  \ ),($ ;

\textit{variables} \  \  \  \  \  \  \  \ $\  \  \  \  \  \  \  \  \ v_{0},v_{1},\ldots
,v_{n},\ldots $ ;

$0$\textit{-ary} \textit{connective} \  \  \ $\  \  \  \  \bot $ $\left( falsity,%
\text{ }falsum,\text{ }absurdum\right) $ ;

\textit{binary} \textit{connective} \  \  \ $\  \  \longrightarrow $ $\left(
implication\right) $ ;

\textit{universal quantifier} \  \ $\  \forall $ $.$

The basic definitions and conventions of $\mathcal{L}$ are as usual (see $%
\left[ 2\right] $); in particular, $\lnot \varphi ,$ $\varphi \vee \psi ,$ $%
\varphi \wedge \psi $ and $\left( \exists v_{i}\right) \varphi \left(
v_{i}\right) $ abbreviate, respectively, $\varphi \longrightarrow \bot ,$ $%
\lnot \varphi \longrightarrow \psi ,$ $\lnot \left( \lnot \varphi \vee \lnot
\psi \right) $ and $\lnot \left( \forall v_{i}\right) \lnot \varphi \left(
v_{i}\right) $ .

$TERM\left( \mathcal{L}^{\prime }\right) ,$ $TERM_{C}\left( \mathcal{L}%
^{\prime }\right) ,$ $ATOM\left( \mathcal{L}^{\prime }\right) ,$ $FORM\left( 
\mathcal{L}^{\prime }\right) ,$ $Sent\left( \mathcal{L}^{\prime }\right) ,$ $%
At\left( \mathcal{L}^{\prime }\right) $ denote, respectively, the classes of
the terms, the closed terms, the atomic formulae, the formulae, the
sentences and the atomic sentences of whatever first-order language $%
\mathcal{L}^{\prime }$ we are using.

\bigskip

\textbf{Definition 1.1. }Let $P$ be a set and $\leq $ a total, dense,
preordering relation on $P$.

$p<q$ and $p=_{\leq }q$ abbreviate, respectively:

$p\leq q\underset{\_}{\wedge }\underset{\_}{\lnot }$ $q\leq p$ and $p\leq q$ 
$\underset{\_}{\mathbf{\wedge }}$ $q\leq p$ $\  \footnote[1]{%
Underlined connectives, quantifiers or equality (meaning identity) belong to
the metalanguage.}$, for each $p,q\in P.$

\newpage

$P$ has a $\leq -$ minimal element $0_{\leq }$ and no $\leq -$ maximal
element; more explicitely:

$\left( \underset{\_}{\forall }p\in P\right) \left( p\leq 0_{\leq }\underset{%
\_}{\longrightarrow }p=_{\leq }0_{\leq }\right) ,$

$\underset{\_}{\lnot }\left( \underset{\_}{\exists }q\in P\right) \left( 
\underset{\_}{\forall }p\in P\right) \left( q\leq p\underset{\_}{%
\longrightarrow }p=_{\leq }q\right) .$

Consider a class valued function $D$ defined on $P$ such that, for each $%
p\in P$, $D\left( p\right) $ is a non-empty class.

For $P,\leq ,D,0_{\leq }$ as described above, an informal sequence $\mathcal{%
F}:\underset{\_}{=}\nolinebreak \left( P,\leq ,D,0_{\leq }\right) $ is
called a \textit{stratifying frame}.

The elements of $P$ are the \textit{nodes} of $\mathcal{F}$ and for each $%
p\in P,$ $D\left( p\right) $ is the \textit{domain }of $\mathcal{F}$ at $p$ $%
.$

\bigskip

\textbf{Definition 1.2. }Let\textbf{\ }$\mathcal{F}\underset{\_}{=}\left(
P,\leq ,D,0_{\leq }\right) $ be a stratifying frame\textbf{.}

To each $a\in D\left( p\right) $ we associate a constant symbol $\overset{\_}%
{a}$ (different constant symbols for different elements of $D\left( p\right) 
$). If $a\in D\left( p\right) $ and $a\in D\left( q\right) $, then the
constant symbol associated with $a$ is the same.

$\mathcal{L}_{\ast },$ $\left( \mathcal{L}_{\ast }\right) _{p}$(for each $%
p\in P)$ and $\left( \mathcal{L}_{\ast }\right) _{+}$ are first-order
extensions of $\mathcal{L}$ defined as:

$\mathcal{L}_{\ast }:\underset{\_}{=}\mathcal{L}$ $\mathcal{\cup }\left \{ 
\mathbf{0,}\sqsubseteq \right \} ,$ where $\mathbf{0}$ is a constant\textit{%
\ }symbol and $\sqsubseteq $ is a \textit{new }binary relation symbol called 
\textit{precedence of level};

$\left( \mathcal{L}_{\ast }\right) _{p}:\underset{\_}{=}\mathcal{L}_{\ast }$ 
$\mathcal{\cup }\left \{ \overset{\_}{a}:a\in D\left( p\right) \right \} $;

\begin{equation*}
\left( \mathcal{L}_{\ast }\right) _{+}:\underset{\_}{=}\underset{p\in P}{%
\cup }\left( \mathcal{L}_{\ast }\right) _{p}.
\end{equation*}

$\mathcal{L}_{\ast }$ is the \textit{stratifying language }associated with $%
\mathcal{L}$ $.$

So, the class of all closed terms of $\left( \mathcal{L}_{\ast }\right) _{+}$
is:%
\begin{equation*}
TERM_{C}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) \underset{\_}{=}%
\left \{ \overset{\_}{a}:\left( \underset{\_}{\exists }p\in P\right) a\in
D\left( p\right) \right \} \cup \left \{ \mathbf{0}\right \} .
\end{equation*}

For any terms $t_{1},t_{2}\in TERM\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) :$

\begin{equation*}
t_{1}\sqsubset t_{2}\text{ abbreviates }t_{1}\sqsubseteq t_{2}\wedge \lnot 
\text{ }t_{2}\sqsubseteq \nolinebreak t_{1}\text{ }.
\end{equation*}

($t_{1}\sqsubseteq t_{2}$ and $t_{1}\sqsubset t_{2}$ must be read,
respectively, as "$t_{1}$ \textit{precedes }$t_{2}$" and "$t_{1}$ \textit{%
strictly precedes }$t_{2}$").

Consider a function $\mathbf{V}$ defined on $TERM_{C}\left( \left( \mathcal{L%
}_{\ast }\right) _{+}\right) $ and with values in $P$ such that $\mathbf{V}%
\left( \mathbf{0}\right) =0_{\leq },$ $a\in D\left( \mathbf{V}\left( \overset%
{\_}{a}\right) \right) $ and for each $p\in P:$

$a\in D\left( p\right) \underset{\_}{\longrightarrow }\mathbf{V}\left( 
\overset{\_}{a}\right) \leq p\underset{\_}{\wedge }\left( \underset{\_}{%
\forall }q\in P\right) \left( q<\mathbf{V}\left( \overset{\_}{a}\right) 
\underset{\_}{\longrightarrow }\underset{\_}{\lnot }\text{ }a\in D\left(
q\right) \right) .$

$\mathbf{V}\left( \overset{\_}{a}\right) $ must be thought as \textit{"the"
\  \footnote[2]{%
The definite article refers to the binary relation $=_{\leq }.$}} \textit{%
first level of interpretation }of $\overset{\_}{a}$ $.$

Consider a function $\Sigma $ defined on $P$ such that, for each $p\in P$, $%
\Sigma \left( p\right) \subseteq \nolinebreak At\left( \left( \mathcal{L}%
_{\ast }\right) _{p}\right) ,$ where $At\left( \left( \mathcal{L}_{\ast
}\right) _{p}\right) $ is the class of all atomic sentences of $\left( 
\mathcal{L}_{\ast }\right) _{p}.$

$\Sigma \left( p\right) $ establish, for each $p\in P,$ the "basic truths"
at $p$ $.$

$D$, $\Sigma $ and $\mathbf{V}$ satisfy the following conditions:

\textbf{1) }$p\leq q\underset{\_}{\longrightarrow }D\left( p\right)
\subseteq D\left( q\right) ,$

\textbf{2)} $\left( \underset{\_}{\forall }p\in P\right) \underset{\_}{\lnot 
}$ $\bot \in \Sigma \left( p\right) ,$

\textbf{3) }$p\leq q\underset{\_}{\longrightarrow }\Sigma \left( p\right)
\subseteq \Sigma \left( q\right) ,$

\textbf{4) }$\overset{\_}{a}_{1}=\overset{\_}{a}_{2}\in \Sigma \left(
p\right) \underset{\_}{\longleftrightarrow }\mathbf{V}\left( \overset{\_}{a}%
_{1}\right) \leq p\underset{\_}{\wedge }\mathbf{V}\left( \overset{\_}{a}%
_{2}\right) \leq p\underset{\_}{\wedge }a_{1}\underset{\_}{=}a_{2}$ $,$

\textbf{5}) $\overset{\_}{a}_{1}\sqsubseteq \overset{\_}{a}_{2}\in \Sigma
\left( p\right) \underset{\_}{\longleftrightarrow }\mathbf{V}\left( \overset{%
\_}{a}_{1}\right) \leq \mathbf{V}\left( \overset{\_}{a}_{2}\right) \leq p$ $%
, $

\textbf{6) }If $R_{i}$ is a $n_{i}$-ary relation symbol of $\mathcal{L}$, $%
a_{1},\ldots ,a_{n_{i}},b_{1},\ldots ,b_{n_{i}}\in D\left( p\right) $ and $%
a_{1}\underset{\_}{=}b_{1},\ldots ,a_{n_{i}}\underset{\_}{=}b_{n_{i}}$ ,
then:

$R_{i}\left( \overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n_{i}}\right) \in
\Sigma \left( p\right) \underset{\_}{\longrightarrow }R\left( \overset{\_}{b}%
_{1},\cdots ,\overset{\_}{b}_{n_{i}}\right) \in \Sigma \left( p\right) .$

(Evidently, if $R_{i}$ is a $n_{i}$-ary relation symbol of $\mathcal{L}$ and 
$R_{i}\left( \overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n_{i}}\right) \in
\nolinebreak \Sigma \left( p\right) ,$ \nolinebreak then:

$\mathbf{V}\left( \overset{\_}{a}_{1}\right) \leq p\underset{\_}{\wedge }%
\cdots \underset{\_}{\wedge }\mathbf{V}\left( \overset{\_}{a}_{n_{i}}\right)
\leq p,$ since $\Sigma \left( p\right) \subseteq At\left( \left( \mathcal{L}%
_{\ast }\right) _{p}\right) $)$.$

\bigskip

\textbf{Definition 1.3. }For $P,\leq ,D,$ $\Sigma ,$ $\mathbf{V,}0_{\leq }$
as described in \textbf{definition 1.1} and \textbf{definition 1.2}, let $%
\mathcal{F}=\left( P,\leq ,D,0_{\leq }\right) $ be a stratifying frame.

A \textit{stratified model }for $\mathcal{L}_{\ast }$ is an informal
sequence $\mathcal{S}_{\ast }:\underset{\_}{=}\left( \mathcal{F},\Sigma ,%
\mathbf{V,}0\right) $ such that

\textbf{1) }$0\in D\left( 0_{\leq }\right) ,$

\textbf{2) }$\overset{\_}{0}$ is identified with $\mathbf{0}.$

The \textit{nodes }of $\mathcal{S}_{\ast }$\ and the \textit{domain }of $%
\mathcal{S}_{\ast }$ at each $p\in P$ are those of $\mathcal{F}$.

\bigskip

\textbf{Remark 1.4. }If $\mathcal{S}_{\ast }\underset{\_}{=}\left( \mathcal{F%
},\Sigma ,\mathbf{V,}0\right) $ is a stratified model for $\mathcal{L}_{\ast
},$ then it is easy to prove that $P$ is an infinite set and, at each $p\in
P,$ $D$ and $\Sigma $ determine a classical structure (see $\left[ 1\right] $%
) $\mathfrak{A}_{p}$ such that $\left \vert \mathfrak{A}_{p}\right \vert 
\underset{\_}{=}D\left( p\right) $ and:

\textbf{i) }$p\leq q\underset{\_}{\longrightarrow }\left \vert \mathfrak{A}%
_{p}\right \vert \subseteq \left \vert \mathfrak{A}_{q}\right \vert .$

\textbf{ii) }The interpretations $R_{i}^{\mathfrak{A}_{p}}$ of a $n_{i}$-ary
relation symbol $R_{i}$ of $\mathcal{L}$ and $\sqsubseteq ^{\mathfrak{A}%
_{p}} $ of $\sqsubseteq $ are:

$\left \langle a_{1},\cdots ,a_{n_{i}}\right \rangle \in R_{i}^{\mathfrak{A}%
_{p}}\underset{\_}{:\longleftrightarrow }R_{i}\left( \overset{\_}{a}%
_{1},\cdots ,\overset{\_}{a}_{n_{i}}\right) \in \Sigma \left( p\right) ,$

$\left \langle a_{1},a_{2}\right \rangle \in \sqsubseteq ^{\mathfrak{A}_{p}}%
\underset{\_}{:\longleftrightarrow }\overset{\_}{a}_{1}\sqsubseteq \overset{%
\_}{a}_{2}\in \Sigma \left( p\right) .$

So, we have

$p\leq q\underset{\_}{\longrightarrow }R_{i}^{\mathfrak{A}_{p}}\subseteq
R_{i}^{\mathfrak{A}_{q}}\underset{\_}{\wedge }$ $\sqsubseteq ^{\mathfrak{A}%
_{p}}\subseteq $ $\sqsubseteq ^{\mathfrak{A}_{p}}.$

\textbf{iii) }$\left( \underset{\_}{\forall }p\in P\right) \left( \underset{%
\_}{\forall }a\in D\left( p\right) \right) \overset{\_}{a}^{\mathfrak{A}%
_{p}}:\underset{\_}{=}a$ ; in particular, since $\mathbf{0}$ is $\overset{\_}%
{0}$ :

\textbf{iv) }$\left( \underset{\_}{\forall }p\in P\right) \mathbf{0}^{%
\mathfrak{A}_{p}}:\underset{\_}{=}0$ .

\bigskip

\newpage

\textbf{Proposition 1.5. }Let $\mathcal{S}_{\ast }\underset{\_}{=}\left( 
\mathcal{F},\Sigma ,\mathbf{V,}0\right) $ be a stratified model\textit{\ }%
for $\mathcal{L}_{\ast }$ .

\textbf{1) }If $\overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n}\in
TERM_{C}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) ,$ then there
is a $p\in P$ such that:

$\left( \ast \right) $ $\ a_{1},\cdots ,a_{n}\in D\left( p\right) \underset{%
\_}{\wedge }\left( \underset{\_}{\forall }q\in P\right) \left( a_{1},\cdots
,a_{n}\in D\left( q\right) \underset{\_}{\longrightarrow }p\leq q\right) .$

\textbf{2) }If $\overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n}\in
TERM_{C}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) ,$ then there
is a $p\in P$ such that:

$\mathbf{V}\left( \overset{\_}{a}_{1}\right) \leq p$ $\underset{\_}{\wedge }%
\cdots \underset{\_}{\wedge }$ $\mathbf{V}\left( \overset{\_}{a}_{n}\right)
\leq p$ $\underset{\_}{\wedge }$ $\left( \underset{\_}{\forall }q\in
P\right) \left( \mathbf{V}\left( \overset{\_}{a}_{1}\right) \leq q\underset{%
\_}{\wedge }\cdots \underset{\_}{\wedge }\mathbf{V}\left( \overset{\_}{a}%
_{n}\right) \leq q\underset{\_}{\longrightarrow }p\leq q\right) .$

\textbf{3)} If $p_{1},p_{2}\in P$ satisfy $\left( \ast \right) $, then $%
p_{1}=_{\leq }p_{2}$ .

\bigskip

\textbf{Proof.}

\textbf{1) }We simply choose $p$ as "the" greatest of all the $\mathbf{V}%
\left( \overset{\_}{a}_{1}\right) ,\cdots ,\mathbf{V}\left( \overset{\_}{a}%
_{n}\right) .$

\textbf{2) }is a reformulation of \textbf{1)} and \textbf{3) }is a direct
consequence of $\left( \ast \right) .$ $\square $

\bigskip

\textbf{Definition 1.6. }If $\mathcal{S}_{\ast }\underset{\_}{=}\left( 
\mathcal{F},\Sigma ,\mathbf{V,}0\right) $ is a stratified model\textit{\ }%
for $\mathcal{L}_{\ast }$ and\textbf{\ }$\overset{\_}{a}_{1},\cdots ,\overset%
{\_}{a}_{n}\in \nolinebreak TERM_{C}\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) ,$ we define $\mathbf{V}\left( \overset{\_}{a}_{1},\cdots ,%
\overset{\_}{a}_{n}\right) $ as "the" $p$ , unique modulo $=_{\leq }$ ,
satisfying $\left( \ast \right) $ in \textbf{proposition 1.5.\nolinebreak }

$\left( \mathbf{V}\left( \overset{\_}{a}_{1},\cdots ,\overset{\_}{a}%
_{n}\right) \text{ is "the" \textit{first level of interpretation of all the}
}\overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n}\right) .$

\bigskip

\textbf{2. Stratified Semantics}

\textbf{Proposition 2.1. }Let $\mathcal{S}_{\ast }\underset{\_}{=}\left( 
\mathcal{F},\Sigma ,\mathbf{V,}0\right) $ be a stratified model for $%
\mathcal{L}_{\ast }$ . Then there exists a unique function $\Sigma ^{\ast }$%
, defined on $P$, such that for each $p\in P,$ $\Sigma \left( p\right)
\subseteq \Sigma ^{\ast }\left( p\right) \subseteq Sent\left( \left( 
\mathcal{L}_{\ast }\right) _{p}\right) $ and

\textbf{i)} $\varphi \in \left( At\left( \left( \mathcal{L}_{\ast }\right)
_{p}\right) \right) \underset{\_}{\wedge }\underset{\_}{\lnot }$ $\varphi
\in \Sigma \left( p\right) \underset{\_}{\longrightarrow }\underset{\_}{%
\lnot }$ $\varphi \in \Sigma ^{\ast }\left( p\right) ,$

\textbf{ii) }$\varphi \longrightarrow \psi \in \Sigma ^{\ast }\left(
p\right) \underset{\_}{\longleftrightarrow }\left( \varphi \in \Sigma ^{\ast
}\left( p\right) \underset{\_}{\longrightarrow }\psi \in \Sigma ^{\ast
}\left( p\right) \right) ,$

\textbf{iii) }$\left( \forall v_{i}\right) \varphi \left( v_{i}\right) \in
\Sigma ^{\ast }\left( p\right) \underset{\_}{\longleftrightarrow }\left( 
\underset{\_}{\forall }a\in D\left( p\right) \right) \varphi \left( \overset{%
\_}{a}\right) \in \Sigma ^{\ast }\left( p\right) .$

\bigskip

\textbf{Proof. }We simply define $\varphi \in \Sigma ^{\ast }\left( p\right)
,$ for each $p\in P,$ by induction on $\varphi $ $.$ $\square $

\bigskip

\textbf{Notation \  \footnote[3]{%
For a \textit{modal view }of \textit{forcing}, see $\left[ 6\right] .$}. }We
write $p\Vdash \varphi $ for $\varphi \in \Sigma ^{\ast }\left( p\right) $
(read "$p$ \textit{forces} $\varphi $").

\bigskip

So, we have, for each $p\in P$ :

\textbf{i) }$p\Vdash \overset{\_}{a}_{1}=$ $\overset{\_}{a}_{2}\underset{\_}{%
\longleftrightarrow }\mathbf{V}\left( \overset{\_}{a}_{1}\right) \leq p%
\underset{\_}{\wedge }\mathbf{V}\left( \overset{\_}{a}_{2}\right) \leq p$ $%
\underset{\_}{\wedge }$ $a_{1}\underset{\_}{=}a_{2}$ .

\textbf{ii) }$p\Vdash \overset{\_}{a}_{1}\sqsubseteq \overset{\_}{a}_{2}%
\underset{\_}{\longleftrightarrow }\mathbf{V}\left( \overset{\_}{a}%
_{1}\right) \leq \mathbf{V}\left( \overset{\_}{a}_{2}\right) \leq p$ .

\textbf{iii) }$\underset{\_}{\lnot }$ $p\Vdash \bot $ $.$

\textbf{iv) }$p\Vdash \varphi \longrightarrow \psi \underset{\_}{%
\longleftrightarrow }\left( p\Vdash \varphi \underset{\_}{\longrightarrow }%
p\Vdash \psi \right) .$

\textbf{v) }$p\Vdash \left( \forall v_{i}\right) \varphi \left( v_{i}\right) 
\underset{\_}{\longleftrightarrow }\left( \underset{\_}{\forall }a\in
D\left( p\right) \right) p\Vdash \varphi \left( \overset{\_}{a}\right) .$

\bigskip

\textbf{Corollary 2.2.}

\textbf{1) }$p\Vdash \lnot \varphi \underset{\_}{\longleftrightarrow }%
\underset{\_}{\lnot }$ $p\Vdash \varphi $ $.$

\textbf{2) }$p\Vdash \lnot \lnot \varphi \underset{\_}{\longleftrightarrow }%
p\Vdash \varphi $ $.$

\textbf{3) }$p\Vdash \varphi \vee \psi \underset{\_}{\longleftrightarrow }%
p\Vdash \varphi \underset{\_}{\vee }p\Vdash \psi $ .

\textbf{4) }$p\Vdash \varphi \wedge \psi \underset{\_}{\longleftrightarrow }%
p\Vdash \varphi \underset{\_}{\wedge }p\Vdash \psi $ .

\textbf{5) }$p\Vdash \left( \exists v_{i}\right) \varphi \left( v_{i}\right) 
\underset{\_}{\longleftrightarrow }\left( \underset{\_}{\exists }a\in
D\left( p\right) \right) p\Vdash \varphi \left( \overset{\_}{a}\right) .$

\textbf{6) }$\mathbf{V}\left( \overset{\_}{a}_{1}\right) \Vdash \overset{\_}{%
a}_{1}\sqsubseteq $ $\overset{\_}{a}_{2}\underset{\_}{\longleftrightarrow }%
\mathbf{V}\left( \overset{\_}{a}_{1}\right) =_{\leq }\mathbf{V}\left( 
\overset{\_}{a}_{2}\right) .$

\textbf{7) }$\mathbf{V}\left( \overset{\_}{a}_{2}\right) \Vdash \overset{\_}{%
a}_{1}\sqsubseteq \overset{\_}{\text{ }a}_{2}\underset{\_}{%
\longleftrightarrow }\mathbf{V}\left( \overset{\_}{a}_{1}\right) \leq 
\mathbf{V}\left( \overset{\_}{a}_{2}\right) .$

\textbf{8) }$p\Vdash \overset{\_}{a}_{1}\sqsubset $ $\overset{\_}{a}_{2}%
\underset{\_}{\longleftrightarrow }\mathbf{V}\left( \overset{\_}{a}%
_{1}\right) <\mathbf{V}\left( \overset{\_}{a}_{2}\right) \leq p$ $.$

\bigskip

\textbf{Proof. }Quite straightforward. $\square $

\bigskip

\textbf{Definition 2.3. }If $\mathcal{S}_{\ast }\underset{\_}{=}\left( 
\mathcal{F},\Sigma ,\mathbf{V},0\right) $ is a stratified model for $%
\mathcal{L}_{\ast }$ and $\varphi \in \nolinebreak FORM\left( \mathcal{L}%
_{\ast }\right) $\nolinebreak \ $\  \footnote[4]{$\left( \underset{\_}{%
\forall }p\in P\right) \left( Sent\left( \mathcal{L}_{\ast }\right)
\subseteq Sent\left( \left( \mathcal{L}_{\ast }\right) _{p}\right) \underset{%
\_}{\wedge }FORM\left( \mathcal{L}_{\ast }\right) \subseteq FORM\left(
\left( \mathcal{L}_{\ast }\right) _{p}\right) \right) .$}$, we define:

$p\Vdash \varphi :\underset{\_}{\longleftrightarrow }p\Vdash \mathcal{C}%
l\left( \varphi \right) $ , where $\mathcal{C}l\left( \varphi \right) $ is
the \textit{universal closure} of $\varphi $ $.$

\bigskip

\textbf{Proposition 2.4. }Let $\mathcal{S}_{\ast }\underset{\_}{=}\left( 
\mathcal{F},\Sigma ,\mathbf{V},0\right) $ be a stratified model for $%
\mathcal{L}_{\ast }$ . Then, if $\ v_{i}$ and $v_{j}$ are different
variables of $\mathcal{L}:$

\textbf{1) }$p\Vdash v_{i}\sqsubseteq v_{i}$ , for each $p\in P.$

\textbf{2) }$p\Vdash v_{i}\sqsubseteq v_{j}:\underset{\_}{%
\longleftrightarrow }\left( \underset{\_}{\forall }a,b\in D\left( p\right)
\right) \mathbf{V}\left( \overset{\_}{a}\right) =_{\leq }\mathbf{V}\left( 
\overset{\_}{b}\right) .$

\textbf{3) }$p\Vdash v_{i}\sqsubseteq \mathbf{0}:\underset{\_}{%
\longleftrightarrow }\left( \underset{\_}{\forall }a\in D\left( p\right)
\right) \mathbf{V}\left( \overset{\_}{a}\right) =_{\leq }0_{\leq }$ $.$

\textbf{4) }$p\Vdash \mathbf{0}\sqsubseteq v_{i}$ $,$ for each $p\in P.$

\bigskip

\textbf{Proof. }Quite straightforward. $\square $

\bigskip

\textbf{Definition 2.5. }Let $\mathcal{F}\underset{\_}{=}\left( P,\leq
,D,0_{\leq }\right) $ be a stratifying frame\textit{.}

The classes of the \textit{elementary progressive} and the \textit{%
elementary regressive} sentences of $\left( \mathcal{L}_{\ast }\right) _{+}$
, denoted, respectively, by $\mathit{Prg}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) $ and $\mathit{Rgr}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) $, are defined inductively:

\textbf{P1) }If $\varphi \in At\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) $, then $\varphi \in \mathit{Prg}_{0}\left( \left( \mathcal{L}%
_{\ast }\right) _{+}\right) ,$

\textbf{P2) }If $\varphi _{1},\varphi _{2}\in \mathit{Prg}_{0}\left( \left( 
\mathcal{L}_{\ast }\right) _{+}\right) $, then $\varphi _{1}\wedge \varphi
_{2},\varphi _{1}\vee \varphi _{2}\in \mathit{Prg}_{0}\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) ,$

\textbf{R1) }$\bot \in \mathit{Rgr}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) $ and if $\varphi $ is an atomic sentence of $\left( 
\mathcal{L}_{\ast }\right) _{+}$ , different from $\bot $ , then $\lnot
\varphi \in \mathit{Rgr}_{0}\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) ,$

\textbf{R2) }If $\varphi _{1},\varphi _{2}\in \mathit{Rgr}_{0}\left( \left( 
\mathcal{L}_{\ast }\right) _{+}\right) $, then $\varphi _{1}\wedge \varphi
_{2},\varphi _{1}\vee \varphi _{2}\in \mathit{Rgr}_{0}\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) ,$

\newpage

\textbf{PR) }If $\varphi _{1}\in \mathit{Prg}_{0}\left( \left( \mathcal{L}%
_{\ast }\right) _{+}\right) $ and $\varphi _{2}\in \mathit{Rgr}_{0}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) $, then $\varphi
_{1}\longrightarrow \varphi _{2}\in \nolinebreak \mathit{Rgr}_{0}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) ,$

\textbf{RP) }If $\varphi _{1}\in \mathit{Rgr}_{0}\left( \left( \mathcal{L}%
_{\ast }\right) _{+}\right) $ and $\varphi _{2}\in \mathit{Prg}_{0}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) $, then $\varphi
_{1}\longrightarrow \varphi _{2}\in \nolinebreak \mathit{Prg}_{0}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) .$

We may now define the classes of the \textit{extended elementary progressive}
and \nolinebreak the \textit{extended elementary regressive} sentences of $%
\left( \mathcal{L}_{\ast }\right) _{+}$ , denoted, respec\nolinebreak
tively, by $\mathit{Prg}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) 
$ and $\mathit{Rgr}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) :$

\textbf{Pi) }If $\varphi \in \mathit{Prg}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) $, then $\varphi \in \mathit{Prg}\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) ,$

\textbf{Pii) }If $\varphi \left( v_{i}\right) \in FORM\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) $ is such that for each $p\in P$ and $a\in
D\left( p\right) ,$ $\varphi \left( \overset{\_}{a}\right) \in \mathit{Prg}%
_{0}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) $, then $\left(
\exists v_{i}\right) \varphi \left( v_{i}\right) \in \mathit{Prg}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) .$

\textbf{Ri) }If $\varphi \in \mathit{Rgr}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) $, then $\varphi \in \mathit{Rgr}\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) ,$

\textbf{Rii) }If $\varphi \left( v_{i}\right) \in FORM\left( \left( \mathcal{%
L}_{\ast }\right) _{+}\right) $ is such that for each $p\in P$ and $a\in
D\left( p\right) ,$ $\varphi \left( \overset{\_}{a}\right) \in \mathit{Rgr}%
_{0}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) $, then $\left(
\forall v_{i}\right) \varphi \left( v_{i}\right) \in \mathit{Rgr}\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) .$

\bigskip

\textbf{Proposition 2.6 (}Weak\textbf{\ }Monotonicity of $\Vdash $).

Let $\mathcal{S}_{\ast }\underset{\_}{=}\left( \mathcal{F},\Sigma ,\mathbf{V}%
,0\right) $ be a stratified model for $\mathcal{L}_{\ast }$ $.$

\textbf{1) }If $\varphi \in \mathit{Prg}_{0}\left( \mathcal{L}_{\ast
}\right) $, then for each $p,q\in P:$

\begin{equation*}
p\leq q\underset{\_}{\longrightarrow }\left( p\Vdash \varphi \underset{\_}{%
\longrightarrow }q\Vdash \varphi \right) .
\end{equation*}

\textbf{2) }If $\varphi \in \mathit{Rgr}_{0}\left( \mathcal{L}_{\ast
}\right) $, then for each $p,q\in P:$%
\begin{equation*}
p\leq q\underset{\_}{\longrightarrow }\left( q\Vdash \varphi \underset{\_}{%
\longrightarrow }p\Vdash \varphi \right) .
\end{equation*}

\textbf{3) }If $\varphi \in \mathit{Prg}\left( \mathcal{L}_{\ast }\right) $
or $\varphi \in \mathit{Rgr}\left( \mathcal{L}_{\ast }\right) $, then we
also have weak monotonic\nolinebreak ity of $\Vdash $ as in\textbf{\ 1) }or 
\textbf{2), }respectively.

\bigskip

\textbf{Proof. }

\textbf{1), 2) }We proceed by induction on $\varphi $ $.$

Consider $p\leq q$ $.$

If $\varphi \in At\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) \cap 
\mathit{Prg}_{0}\left( \mathcal{L}_{\ast }\right) $, then \textbf{1)} is
immediate by \textbf{def\nolinebreak inition 1.2, 3) }and\textbf{\
proposition 2.1}.

Of course, \textbf{2)} is satisfied by $\bot $ and if $\varphi \in At\left(
\left( \mathcal{L}_{\ast }\right) _{+}\right) \backslash \left \{ \bot
\right \} $ , then the proof of \textbf{2)} for $\lnot \varphi $ is
immediate by \textbf{def\nolinebreak inition 1.2, 3) }and\textbf{\
proposition 2.1}.

If $\varphi $ is $\varphi _{1}\wedge \varphi _{2}$ $,$ where $\varphi
_{1},\varphi _{2}\in \mathit{Prg}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) ,$ then$:$\newline
$p\Vdash $ $\varphi _{1}\wedge \varphi _{2}\underset{\_}{\longleftrightarrow 
}p\Vdash $ $\varphi _{1}\underset{\_}{\wedge }p\Vdash \varphi _{2}\underset{%
\begin{array}{c}
Ind. \\ 
Hyp.%
\end{array}%
}{\underset{\_}{\longrightarrow }}q\Vdash $ $\varphi _{1}\underset{\_}{%
\wedge }q\Vdash \varphi _{2}\underset{\_}{\longleftrightarrow }q\Vdash
\varphi _{1}\wedge \varphi _{2}$ $.$

If $\varphi $ is $\varphi _{1}\vee \varphi _{2}$ $,$ where $\varphi
_{1},\varphi _{2}\in \mathit{Prg}_{0}\left( \left( \mathcal{L}_{\ast
}\right) _{+}\right) ,$ then$:$\newline
$p\Vdash $ $\varphi _{1}\vee \varphi _{2}\underset{\_}{\longleftrightarrow }%
p\Vdash $ $\varphi _{1}\underset{\_}{\vee }p\Vdash \varphi _{2}\underset{%
\begin{array}{c}
Ind. \\ 
Hyp.%
\end{array}%
}{\underset{\_}{\longrightarrow }}q\Vdash $ $\varphi _{1}\underset{\_}{\vee }%
q\Vdash \varphi _{2}\underset{\_}{\longleftrightarrow }q\Vdash \varphi
_{1}\vee \varphi _{2}$ $.$

If $\varphi $ is $\varphi _{1}\vee \varphi _{2}$ or $\varphi $ is $\varphi
_{1}\wedge \varphi _{2}$ $,$ where $\varphi _{1},\varphi _{2}\in \mathit{Rgr}%
_{0}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) ,$ then we proceed
in a similar manner to prove \textbf{2).}

If $\varphi $ is $\varphi _{1}\longrightarrow \varphi _{2}$ $,$ where $%
\varphi _{1}\in \mathit{Rgr}_{0}\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) $ and $\varphi _{2}\in \mathit{Prg}_{0}\left( \left( \mathcal{L}%
_{\ast }\right) _{+}\right) $, then$:$\newline
$p\Vdash $ $\varphi _{1}\longrightarrow \varphi _{2}\underset{\_}{\wedge }%
q\Vdash $ $\varphi _{1}\underset{\_}{\longrightarrow }p\Vdash \varphi
_{1}\longrightarrow \varphi _{2}\underset{\_}{\wedge }p\Vdash $ $\varphi _{1}%
\underset{\_}{\longrightarrow }p\Vdash $ $\varphi _{2}\underset{\_}{%
\longrightarrow }q\Vdash $ $\nolinebreak \varphi _{2}$ $.$

So:

$p\Vdash $ $\varphi \underset{\_}{\longrightarrow }q\Vdash $ $\varphi $ $.$

Similarly, we prove \textbf{2)} for $\varphi _{1}\longrightarrow \varphi
_{2},$ where $\varphi _{1}\in \mathit{Prg}_{0}\left( \left( \mathcal{L}%
_{\ast }\right) _{+}\right) $ and $\varphi _{2}\in \nolinebreak \mathit{Rgr}%
_{0}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) .$

\textbf{3) }Consider $p\leq q$ $.$

If $\varphi \in \mathit{Prg}_{0}\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) $, then we simply use \textbf{1).}

If $\varphi $ is $\left( \exists v_{i}\right) \varphi _{1}\left(
v_{i}\right) ,$ where $\varphi _{1}\left( v_{i}\right) \in FORM\left( \left( 
\mathcal{L}_{\ast }\right) _{+}\right) $ and for each $r\in P$ and $a\in
D\left( r\right) ,$ $\varphi _{1}\left( \overset{\_}{a}\right) \in \mathit{%
Prg}_{0}\left( \left( \mathcal{L}_{\ast }\right) _{+}\right) ,$ then$:$%
\newline
$p\Vdash \left( \exists v_{i}\right) \varphi _{1}\left( v_{i}\right) 
\underset{\_}{\longleftrightarrow }\left( \underset{\_}{\exists }a\in
D\left( p\right) \right) p\Vdash \varphi _{1}\left( \overset{\_}{a}\right) 
\underset{%
\begin{array}{c}
\text{\textbf{1)}} \\ 
D\left( p\right) \subseteq D\left( q\right)%
\end{array}%
}{\underset{\_}{\longrightarrow }}\left( \underset{\_}{\exists }a\in D\left(
q\right) \right) q\Vdash \nolinebreak \varphi _{1}\left( \overset{\_}{a}%
\right) \underset{\_}{\longleftrightarrow }$\newline
$\underset{\_}{\longleftrightarrow }q\Vdash \left( \exists v_{i}\right)
\varphi _{1}\left( v_{i}\right) .$

If $\varphi \in \mathit{Rgr}\left( \left( \mathcal{L}_{\ast }\right)
_{+}\right) $ we proceed \textit{mutatis mutandis} in the same manner. $%
\square $

\bigskip

\textbf{Definition 2.7.}

\textbf{1) }If $\varphi \in Sent\left( \mathcal{L}_{\ast }\right) $ and $%
\mathcal{S}_{\ast }\underset{\_}{=}\left( \mathcal{F},\Sigma ,\mathbf{V}%
,0\right) $ is a stratified model for $\mathcal{L}_{\ast }$ $,$ we define $%
\mathcal{S}_{\ast }$ $\mathcal{\Vdash \varphi }$ (read "$\mathcal{S}_{\ast }$
\textit{forces} $\varphi $" or "$\mathcal{S}_{\ast }$ \textit{is a
stratified model} \textit{of} $\varphi $") as:%
\begin{equation*}
\mathcal{S}_{\ast }\text{ }\mathcal{\Vdash \varphi }\underset{\_}{%
:\longleftrightarrow }\left( \underset{\_}{\forall }p\in P\right) p\Vdash
\varphi \text{ .}
\end{equation*}

We also\textbf{\ }define $\mathcal{\Vdash \varphi }$ (read "$\varphi $ 
\textit{is} \textit{universally valid}" or "$\varphi $ \textit{is} \textit{%
valid}") as:

$\mathcal{\Vdash \varphi }\underset{\_}{:\longleftrightarrow }\left( 
\underset{\_}{\forall }\mathcal{S}_{\ast }\right) \mathcal{S}_{\ast }\Vdash
\varphi $ $,$ where the possible values of the metavariable $\mathcal{S}%
_{\ast }$ are all stratified models for $\mathcal{L}_{\ast }$ .

If $\Sigma $ is a subset of $Sent\left( \mathcal{L}_{\ast }\right) ,$ we
define $\mathcal{S}_{\ast }$ $\mathcal{\Vdash }$ $\Sigma $ (read "$\mathcal{S%
}_{\ast }$ \textit{forces} $\Sigma $" or "$\mathcal{S}_{\ast }$ \textit{is a
stratified model} \textit{of} $\Sigma $") as:

\begin{equation*}
\mathcal{S}_{\ast }\text{ }\mathcal{\Vdash }\text{ }\Sigma \underset{\_}{%
:\longleftrightarrow }\left( \underset{\_}{\forall }\varphi \in \Sigma
\right) \mathcal{S}_{\ast }\text{ }\mathcal{\Vdash \varphi }\text{ }.
\end{equation*}

\textbf{2) }If $\Gamma $ $\cup $ $\left \{ \varphi \right \} \subseteq
Sent\left( \mathcal{L}_{\ast }\right) ,$ we define $\Gamma \Vdash \varphi $
(read "$\varphi $ \textit{is a} \textit{stratified logical consequence of} $%
\Gamma $") as:

\begin{equation*}
\Gamma \Vdash \varphi :\underset{\_}{\longleftrightarrow }\left( \underset{\_%
}{\forall }\mathcal{S}_{\ast }\right) {\LARGE (}\mathcal{S}_{\ast }\Vdash
\Gamma \underset{\_}{\longrightarrow }\mathcal{S}_{\ast }\Vdash \varphi 
{\LARGE )}.
\end{equation*}

If $\Gamma $ $\cup $ $\left \{ \varphi \right \} \subseteq FORM\left( 
\mathcal{L}_{\ast }\right) $\ and $FV\left( \Gamma \cup \left \{ \varphi
\right \} \right) =\left \{ v_{i_{1}},\ldots ,v_{i_{n}}\right \} ,$ where $%
FV\left( \Gamma \cup \left \{ \varphi \right \} \right) $ is the set of all
free variables of $\Gamma \cup \left \{ \varphi \right \} ,$ we define $%
\Gamma \Vdash \varphi $ (read "$\varphi $ \textit{is a} \textit{stratified
logical consequence of} $\Gamma $") as:

$\Gamma \Vdash \varphi :\underset{\_}{\longleftrightarrow }\left( \underset{%
\_}{\forall }\mathcal{S}_{\ast }\right) \left( \underset{\_}{\forall }p\in
P\right) \left( \underset{\_}{\forall }a_{1},\cdots ,a_{n}\in D\left(
p\right) \right) {\LARGE (}p\Vdash \nolinebreak \Gamma \left( \overset{\_}{%
\overrightarrow{a}}\right) \underset{\_}{\longrightarrow }\nolinebreak
p\Vdash $\nolinebreak $\varphi \left( \overset{\_}{\overrightarrow{a}}%
\right) {\LARGE )},$ where $\overset{\_}{\overrightarrow{a}}\underset{\_}{=}%
\left \langle \overset{\_}{a}_{1},\cdots ,\overset{\_}{a}_{n}\right \rangle
, $ and $p\Vdash \Gamma \left( \overset{\_}{\overrightarrow{a}}\right) $
abbreviates $\left( \underset{\_}{\forall }\psi \in \Gamma \right) p\Vdash
\nolinebreak \psi \left( \overset{\_}{\overrightarrow{a}}\right) .$

\bigskip

\textbf{3. Soundness, Conservativeness and Completeness.}

Before we investigate \textit{soundness}, let us exhibit the \textit{rules
of inference} we are using in a context of \textit{natural deduction }(using%
\textit{\ }the\textit{\ }language $\mathcal{L}_{\ast }$) and with the usual
notion of \textit{derivation \  \footnote[5]{%
Remember that, in particular, derivations are finite trees of formulae and $%
\Gamma $ may have superfluous hypotheses.}:}%
\begin{equation*}
\text{\textbf{Introduction Rules}}
\end{equation*}

\textbf{1)} $\left( \longrightarrow I\right) $ $\left[ \varphi \right] $ $\ 
\footnote[6]{%
Hypotheses enclosed in square brackets are cancelable.}$ \  \  \  \  \  \  \  \  \  \
\  \  \vspace{0.1in}\textbf{2)} $\left( \forall I\right) $ $\dfrac{\varphi }{%
\left( \forall v_{i}\right) \varphi }$

\vspace{0.2in}\vspace{-1in}\vspace{0.5in}\vspace{0.01in}\vspace{0.02in}\  \  \
\  \  \  \  \  \  \  \  \  \  \  \  \ $\vdots $

\  \  \  \  \  \  \ $\dfrac{\text{ \  \ }\psi }{\text{ \  \  \  \ }\varphi
\longrightarrow \psi }$

\begin{equation*}
\text{\textbf{Elimination Rule\textbf{s}}}
\end{equation*}

\textbf{3) }$\left( \longrightarrow E\right) $ $\dfrac{\varphi \text{ \ }%
\varphi \longrightarrow \psi }{\psi }$ \  \  \  \textbf{4) }$\left( \bot
\right) $ $\dfrac{\bot }{\varphi }$

\bigskip

\vspace{-0.2cm}\textbf{5)} $\left( RAA\right) $ $\left[ \lnot \varphi \right]
$ \  \  \  \  \  \  \  \  \  \  \  \  \  \  \textbf{6) }$\left( \forall E\right) $ $\dfrac{%
\left( \forall v_{i}\right) \varphi }{\varphi \left[ t/v_{i}\right] }$

\vspace{-0.2in}\  \  \  \  \  \  \  \  \  \  \  \  \  \  \  \  \ $\vdots $

$\vspace{-0.2in}\  \  \  \  \  \  \  \  \  \  \  \  \  \  \  \  \dfrac{\bot }{\varphi }$

\bigskip

\vspace{0.05cm}\vspace{0.1cm}The axioms for $=$ and $\sqsubseteq $ are also
presented as rules of infer\nolinebreak ence:%
\begin{equation*}
\text{\textbf{Equality Rule\textbf{s}}}
\end{equation*}

\textbf{7) }$\left( ER_{1}\right) $ $\dfrac{{}}{v_{i}=v_{i}}$ \  \  \  \  \ 
\textbf{8) }$ER_{2}$ $\dfrac{{}}{v_{i}=v_{j}\longrightarrow v_{j}=v_{i}}$ \
\  \  \  \  \textbf{9)} $\left( ER_{3}\right) $ $\dfrac{{}}{v_{i}=v_{j}\wedge
v_{j}=v_{k}\longrightarrow v_{i}=v_{k}}$

\bigskip

\textbf{10) }$\left( ER_{4}\right) $ For each $n_{i}$-ary relation symbol $%
R_{i}$ of $\mathcal{L}:$%
\begin{equation*}
\frac{{}}{v_{j_{1}}=v_{k_{1}}\wedge \ldots \wedge
v_{j_{n_{i}}}=v_{k_{n_{i}}}\wedge R_{i}\left( v_{j_{1}},\ldots
,v_{j_{n_{i}}}\right) \longrightarrow R_{i}\left( v_{k_{1}},\ldots
,v_{k_{n_{i}}}\right) }
\end{equation*}

\textbf{11) }$\left( ER_{5}\right) \dfrac{{}}{v_{i_{1}}=v_{j_{1}}\wedge
v_{i_{2}}=v_{j_{2}}\wedge v_{i_{1}}\sqsubseteq v_{i_{2}}\longrightarrow
v_{j_{1}}\sqsubseteq v_{j_{2}}}$

\bigskip

\begin{equation*}
\text{\textbf{Precedence of Level Rules}}
\end{equation*}

\textbf{12) }$\left( PLR_{1}\right) $ $\dfrac{{}}{v_{i}\sqsubseteq v_{i}}$ \
\  \  \  \  \textbf{13)} $\left( PLR_{2}\right) $ $\dfrac{{}}{v_{i}\sqsubseteq
v_{j}\wedge v_{j}\sqsubseteq v_{k}\longrightarrow v_{i}\sqsubseteq v_{k}}$ \
\  \  \  \ 

\bigskip

\textbf{14)} $\left( PLR_{3}\right) \dfrac{{}}{v_{i}\sqsubseteq v_{j}\vee
v_{j}\sqsubseteq v_{i}}$ \  \  \  \  \  \textbf{15) }$\left( PLR_{4}\right) $ $%
\dfrac{{}}{\mathbf{0}\sqsubseteq v_{i}}$ $\  \  \  \  \ $

\bigskip

\textbf{Restrictions. }In \textbf{2)}, $v_{i}$ does not occur free in any
hypothesis on which $\varphi $ depends and in \textbf{6)}, $t\in TERM\left( 
\mathcal{L}_{\ast }\right) $ is free for $v_{i}$ in $\varphi .$

\bigskip

\newpage

\textbf{Theorem 3.1 (}Soundness\textbf{).} If $\Gamma \cup \left \{ \varphi
\right \} \subseteq FORM\left( \mathcal{L}_{\ast }\right) ,$ then:

\begin{equation*}
\Gamma \vdash \varphi \underset{\_}{\longrightarrow }\Gamma \Vdash \varphi 
\text{ }.
\end{equation*}

\bigskip

\textbf{Proof. }We use induction on the derivation $\mathcal{D}$ of $\varphi 
$ from $\Gamma $. During the proof, we use an arbitrary stratified model $%
\mathcal{S}_{\ast }$.

If $\varphi \in \Gamma $, then we certainly have, with $FV\left( \Gamma \cup
\left \{ \varphi \right \} \right) =\nolinebreak \left \{ v_{i_{1}},\ldots
,v_{i_{n}}\right \} $:

$\left( \underset{\_}{\forall }p\in P\right) \left( \underset{\_}{\forall }%
a_{1},\cdots ,a_{n}\in D\left( p\right) \right) \left( p\Vdash \Gamma \left( 
\overset{\_}{\overrightarrow{a}}\right) \underset{\_}{\longrightarrow }%
p\Vdash \varphi \left( \overset{\_}{\overrightarrow{a}}\right) \right) .$

If the end of $\mathcal{D}$ is an application of a derivation rule, then we
must examine the rules of inference one by one. This is a quite
uncomplicated, albeit tedious, task; for instance:

$\left( \forall I\right) :FV\left( \Gamma \right) =\left \{ v_{i_{1}},\cdots
,v_{i_{n}}\right \} $ and $v_{i}\notin \left \{ v_{i_{1}},\cdots
,v_{i_{n}}\right \} .$

\textbf{Induction hypothesis: }

$\left( \underset{\_}{\forall }p\in P\right) \left( \underset{\_}{\forall }%
a_{1},\cdots ,a_{n},b\in D\left( p\right) \right) \left( p\Vdash \Gamma
\left( \overset{\_}{\overrightarrow{a}}\right) \underset{\_}{\longrightarrow 
}p\Vdash \varphi \left( \overset{\_}{\overrightarrow{a}},\overset{\_}{b}%
\right) \right) .$

Then:

$\left( \underset{\_}{\forall }p\in P\right) \left( \underset{\_}{\forall }%
a_{1},\cdots ,a_{n}\in D\left( p\right) \right) \left( p\Vdash \Gamma \left( 
\overset{\_}{\overrightarrow{a}}\right) \underset{\_}{\longrightarrow }%
\left( \underset{\_}{\forall }b\in D\left( p\right) \right) p\Vdash \varphi
\left( \overset{\_}{\overrightarrow{a}},\overset{\_}{b}\right) \right) .$

Finally:

$\left( \underset{\_}{\forall }p\in P\right) \left( \underset{\_}{\forall }%
a_{1},\cdots ,a_{n}\in D\left( p\right) \right) \left( p\Vdash \Gamma \left( 
\overset{\_}{\overrightarrow{a}}\right) \underset{\_}{\longrightarrow }%
p\Vdash \left( \left( \forall v_{i}\right) \varphi \right) \left( \overset{\_%
}{\overrightarrow{a}}\right) \right) .$ $\square $

\bigskip

\textbf{Theorem 3.2. }If $\Gamma \cup \left \{ \varphi \right \} \subseteq
FORM\left( \mathcal{L}\right) ,$ then:

\textbf{1) (}Conservativeness\textbf{)}%
\begin{equation*}
\Gamma \vdash _{cl}\varphi \underset{-}{\longleftrightarrow }\Gamma \vdash
\varphi ,
\end{equation*}%
where $\Gamma \vdash _{cl}\varphi $ abbreviates "$\varphi $ is derived from $%
\Gamma ,$ in the usual way, using the rules of inference \textbf{1) }to 
\textbf{10)}".

\textbf{2) (}Semantic Extension\textbf{)}%
\begin{equation*}
\Gamma \models \varphi \underset{\_}{\longrightarrow }\Gamma \Vdash \varphi 
\text{ }.
\end{equation*}

If $\varphi $\ is a classical logical consequence of $\Gamma $ then $\varphi 
$ is also a strat\nolinebreak ified logical consequence of $\Gamma .$

\bigskip

\textbf{Proof. }

\textbf{1) }Immediate\textbf{, }because the rules of inference \textbf{1) }%
to \textbf{10)} and the notion of derivation are the same in classical and
in stratified first-order logic.

\textbf{2) }By classical completeness and soundness:%
\begin{equation*}
\Gamma \models \varphi \underset{-}{\longleftrightarrow }\Gamma \vdash
_{cl}\varphi \text{ }.
\end{equation*}

By stratified soundness:%
\begin{equation*}
\Gamma \vdash \varphi \underset{\_}{\longrightarrow }\Gamma \Vdash \varphi 
\text{ }.
\end{equation*}

Finally, using \textbf{1)}:

\begin{equation*}
\Gamma \models \varphi \underset{\_}{\longrightarrow }\Gamma \Vdash \varphi 
\text{ }.\text{ }\square
\end{equation*}%
\bigskip \  \ 

\textbf{Definition 3.3}.

$\mathcal{P}_{c}\left( Sent\left( \mathcal{L}_{\ast }\right) \right) :%
\underset{\_}{=}\left \{ \Sigma \subseteq Sent\left( \mathcal{L}_{\ast
}\right) :\Sigma \text{ has a classical model}\underset{\_}{\longrightarrow }%
\Sigma \text{ has a stratified model}\right \} .$

\bigskip

\textbf{Theorem 3.4 }(Completeness). If $\Gamma $ is a consistent \ 
\footnote[7]{%
Here as elsewhere in this work, "consistent" has the usual meaning in
first-order logic.} subset of $Sent\left( \mathcal{L}_{\ast }\right) $ and $%
\Gamma \cup \left \{ \lnot \varphi \right \} \in \mathcal{P}_{c}\left(
Sent\left( \mathcal{L}_{\ast }\right) \right) ,$ then$:$%
\begin{equation*}
\Gamma \Vdash \varphi \underset{\_}{\longrightarrow }\Gamma \vdash \varphi 
\text{ }.
\end{equation*}%
\ 

\textbf{Proof. }Let $\Gamma \Vdash \varphi $ $.$

If $\underset{\_}{\lnot }$ $\Gamma \vdash \varphi $ $,$ then:%
\begin{equation*}
\Gamma \cup \left \{ \lnot \varphi \right \} \text{ is consistent.}
\end{equation*}

So, $\Gamma \cup \left \{ \lnot \varphi \right \} $ has a classical model.

Since $\Gamma \cup \left \{ \lnot \varphi \right \} \in \mathcal{P}%
_{c}\left( Sent\left( \mathcal{L}_{\ast }\right) \right) ,$ $\Gamma \cup
\left \{ \lnot \varphi \right \} $ has a stratified model, $\mathcal{S}%
_{\ast }$ $.$

But then, $\mathcal{S}_{\ast }$ is a stratified model of $\left \{ \varphi
,\lnot \varphi \right \} $ and that is impossible.

We conclude that:%
\begin{equation*}
\Gamma \vdash \varphi \text{ }.\text{ }\square
\end{equation*}

\bigskip

\textbf{Conclusion.}

The \textit{stratification }presented in this work may be applied to any
theory (in the usual, informal sense, of this word) formalizable in a
first-order language like $\mathcal{L}.$ So, we may stratify $ZFC$ \ 
\footnote[8]{%
For a different approach, see $\left[ 3\right] ,\left[ 4\right] .$} or even
such theories as \textbf{Nelson internal set theory}, $IST$, or \textbf{Hrba%
\v{c}ek set theory}, $HST$, that are largely used in \textit{nonstandard
analysis} (see $\left[ 5\right] $)\textit{.}

\bigskip

\textbf{References}

$\left[ 1\right] $ \ C. C. CHANG \& H. J. KEISLER, \textit{Model Theory, }%
North-Holland,.1973.

$\left[ 2\right] $ \ D. VAN DALEN, \textit{Logic and Structure, }%
Universitext, Springer-Verlag, 1994.

$\left[ 3\right] $ \ K. HRBACEK, Stratified analysis?\textit{, }in:\ I. van
den Berg, V. Neves, ed., \textit{The strength of nonstandard analysis, }%
Springer-Verlag, 2007.

$\left[ 4\right] $ \ K. HRBACEK, Internally Iterated Ultrapowers, in \textit{%
Nonstandard Mod\nolinebreak els of Arithmetic and Set Theory,} ed. by A.
Enayat and R. Kossak Contemporary Math. 361, American Mathematical Society,
Providence, R. I., 2004.

$\left[ 5\right] $ \ V. KANOVEI \& M. REEKEN, \textit{Nonstandard Analysis,
Axiomatically, }Springer-Verlag, 2004.

$\left[ 6\right] $ \ R. SMULLYAN \& M. FITTING, \textit{Set Theory and the
Continuum Prob\nolinebreak lem}, Oxford University Press, 1996.

\end{document}
