1: % First-Order Gödel Logics

2: % Matthias Baaz, Norbert Preining, Richard Zach

3: 

4: \documentclass[final]{article} 

5: \usepackage{amsthm,amsmath,amsfonts,amssymb,xspace,paralist,pictexwd}

6: \usepackage[latin1]{inputenc}

7: \usepackage{textcomp}

8: \usepackage{mathrsfs}

9: \usepackage{fixme,proof}  \usepackage{mathptmx}

10: 

11: %\usepackage{changebar}

12: 

13: \usepackage[scaled=0.92]{helvet}

14: 

15: 

16: %

17: % various definitions

18: %

19: %\let\originallabel\label

20: %\def\label#1{\marginpar{\small label=#1}\originallabel{#1}}

21: 

22: \gdef\NoneSymbol{\hbox{$\Box$}}

23: 

24: %

25: % Theorem stype

26: % alles wird der Reihe nach durchnummeriert!

27: %

28: \newtheorem{theorem}{Theorem}

29: \newtheorem{lemma}[theorem]{Lemma}

30: \newtheorem{proposition}[theorem]{Proposition}

31: \newtheorem{corollary}[theorem]{Corollary}

32: \newtheorem{conjecture}[theorem]{Conjecture}

33: \newtheorem{qu}[theorem]{Questions}

34: \newtheorem{fact}[theorem]{Fact}

35: 

36: \theoremstyle{definition}

37: \newtheorem{definition}[theorem]{Definition}

38: \newtheorem{notation}[theorem]{Notation}

39: 

40: \theoremstyle{remark}

41: \newtheorem*{remark}{Remark}

42: \newtheorem*{example}{Example}

43: %\newtheorem{remark}[theorem]{Remark}

44: 

45: 

46: \let\imm\ensuremath

47: \newcommand\limp{\to}

48: \let\impl\limp

49: \newcommand{\rimpl}{\leftarrow}

50: \newcommand\s{\imm{\mathnormal{\bf s}}}

51: \newcommand\I{\imm{\mathfrak{I}}}

52: \newcommand\J{\imm{\mathfrak{J}}}

53: \def\boeta{{\bf\eta}}

54: \def\one{{{\bf 1}}}

55: \let\val\I

56: \newcommand{\g}{$\mathbf{G}$}

57: %\newcommand\I{v}

58: \newcommand\Distr{{\rm Distr}}

59: %\newcommand\G{\mathbf{G}}

60: \newcommand\LC{\imm{\mathbf{LC}}}

61: \newcommand\Frm{{\rm Frm}}

62: \newcommand\Gd{{\gdl V}}

63: \newcommand\Go{{\mathbf {G}^0}}

64: \newcommand\Gn{{\gdl n}}

65: \newcommand\GR{{\gdl\R}}

66: \newcommand\R{\mathbb{R}}

67: \newcommand\dom{\mathop{\mathrm{dom}}}

68: \def\HU{\mathrm{HU}}

69: \def\HB{\mathrm{HB}}

70: \let\bbR\R

71: \def\up{{\uparrow}}

72: \let\vup\up

73: \def\dn{{\downarrow}}

74: \let\vdn\dn

75: \let\mmodels\models

76: \def\card#1{\lvert #1 \rvert}

77: \def\eval#1{\lvert #1 \rvert}

78: 

79: \def\T{{\bf\sf T}}

80: \def\lo{\mathbf{L}}

81: \newcommand{\modelsg}{\mathrel{\Gd \models}}

82: \newcommand{\modelsl}{\mathrel{\lo \models}}

83: \newcommand{\IMPLIES}{\ \Rightarrow\ }

84: 

85: \def\N{{\mathbb N}}

86: \def\bbZ{{\mathbb Z}}

87: \def\bbD{\mathbb{D}}

88: \let\bbN\N

89: \let\nmodels\nvDash

90: \def\proves{\mathrel{\vdash}}

91: \def\nproves{\mathrel{\nvdash}}

92: \def\entails{\mathrel{\models}}

93: \def\nentails{\mathrel{\nmodels}}

94: \def\dequiv{\Leftrightarrow}

95: \def\lequiv{\leftrightarrow}

96: \def\strc#1#2{\left<#1,#2\right>}

97: \def\Feq{{\cF/\mathnormal{\equiv}}}

98: \def\lF{\strc\Feq\le}

99: 

100: \newcommand\tup[1]{\overline{#1}}

101: \def\Q{{\ensuremath{\mathord{\mathsf{Q}}}}}

102: \newcommand{\LL}{{\mathscr L}}

103: \let\vhi\varphi

104: \newcommand\qe[1]{\exists #1}

105: \newcommand\qa[1]{\forall #1}

106: \newcommand\suchthat{\mathrel{:}}

107: \newcommand{\smc}{smc-}

108: \newcommand{\gdl}[1]{\mathbf {G}_{#1}}

109: %\newcommand{\gdl}[1]{{\bf G}_{#1}}

110: \newcommand\subval{\mathrm{Val}}

111: \newcommand{\bbQ}{\ensuremath{\mathbb{Q}}\xspace}

112: \newcommand{\pfeil}[1]{\mathrel{\mathop{\longrightarrow}\limits^{#1} }}

113: 

114: \newcommand{\IPL}{\mbox{IPL}}

115: \newcommand{\IL}{\mbox{IL}}

116: \def\seq{\mathop{\Rightarrow}}

117: \renewcommand{\H}{\mathbf{H}}

118: \newcommand{\Ho}{{\mathbf{H}_0}}

119: \newcommand{\Hn}{{\mathbf{H}_n}}

120: \newcommand{\cF}{\mathcal{F}}

121: \newcommand{\cR}{\mathcal{R}}

122: \newcommand{\cT}{\mathcal{T}}

123: \newcommand{\cA}{\mathcal{A}}

124: \newcommand{\cD}{\mathcal{D}}

125: \newcommand{\cG}{\mathcal{G}}

126: \newcommand{\cH}{\mathcal{H}}

127: \newcommand{\lOr}{\bigvee}

128: \def\qp{{{qp}}}

129: \def\axlin{{\ensuremath{\hbox{\scshape lin}}}}

130: \def\axiso{{\ensuremath{\hbox{\scshape iso}}}}

131: \def\axqs{{\ensuremath{\hbox{\scshape qs}}}}

132: \def\axqs{{\ensuremath{\hbox{\scshape qs}}}}

133: \def\axqsqp{{\ensuremath{\hbox{\scshape qs}_\qp}}}

134: \def\axlin{{\ensuremath{\hbox{\scshape lin}}}}

135: \def\axiso{{\ensuremath{\hbox{\scshape iso}_0}}}

136: \def\axisoi{{\ensuremath{\hbox{\scshape iso}_1}}}

137: \def\axfinn{{\ensuremath{\hbox{\scshape fin}(n)}}}

138: \def\axdelta{\mathnormal{\upDelta}}

139: \def\axdi{{\ensuremath{\axdelta1}}}

140: \def\axdii{{\ensuremath{\axdelta2}}}

141: \def\axdiii{{\ensuremath{\axdelta3}}}

142: \def\axdiv{{\ensuremath{\axdelta4}}}

143: \def\axdv{{\ensuremath{\axdelta5}}}

144: \def\axdel{{\ensuremath{\hbox{\scshape ax}\axdelta}}}

145: \def\axdense{{\ensuremath{\hbox{\scshape den}}}}

146: \def\one{\mathbf{1}}

147: \def\zero{\mathbf{0}}

148: \def\los#1{\strc{#1}\le}

149: \def\lL{\los L}

150: \def\lQ{\los{[0,1]\cap\bbQ}}

151: \def\lR{\los{[0,1]}}%\cap\bbR}}

152: \def\alepho{{\aleph_0}}

153: \def\lee{\preceq}

154: \def\cbrank#1{|#1|_{\mathrm{CB}}}

155: \def\rg{\mathrm{rg}}

156: \def\lAnd{\bigwedge}

157: 

158: \let\Proves\Rightarrow

159: \let\nProves\nRightarrow

160: 

161: \def\tik#1:{%

162:   \putrule from #1 -2 to #1 +2}

163: \def\Tik#1,#2:{%

164:   \put {$#2$} [b] at #1 5

165:   \putrule from #1 -2 to #1 +4}

166: \def\tiku#1,#2:{%

167:   \put {$#2$} [b] at #1 24

168:   \putrule from #1 18 to #1 22}

169: \def\tikd#1,#2:{%

170:   \put {$\smash{#2}$} at #1 -6

171:   \putrule from #1 -2 to #1 2}

172: \def\tikdd#1,#2:{%

173:   \put {$\smash{#2}$} at #1 4

174:   \putrule from #1 -2 to #1 2}

175: 

176: 

177: 

178: 

179: 

180: 

181: % Local Variables:

182: % TeX-master: "bpz"

183: % End:

184: 

185: 

186: \title{First-Order Gödel Logics}

187: 

188: \author{Matthias Baaz\thanks{Research supported by \textsc{FWF} grant

189: \textsc{P15477--MAT}}\\ 

190: Technische Universität Wien\\ 

191: 1040 Vienna, Austria\\

192: baaz@logic.at \and

193: Norbert Preining%

194: \thanks{Research supported by \textsc{EC-MC 008054}

195:   and \textsc{FWF} grant \textsc{P16539-N04}}\\

196: Università di Siena\\

197: 53100 Siena, Italy\\

198: preining@logic.at \and

199: Richard Zach\thanks{Research supported by the Natural Sciences and Engineering

200:   Research Council of Canada}\\

201: University of Calgary\\

202: Calgary, \textsc{AB T2N 1N4},

203: Canada\\ rzach@ucalgary.ca}

204: 

205: \sloppy

206: 

207: \begin{document}

208: 

209: \maketitle

210: 

211: \begin{abstract} 

212:   First-order Gödel logics are a family of infinite-valued logics where the

213:   sets of truth values~$V$ are closed subsets of $[0, 1]$ containing both $0$

214:   and $1$.  Different such sets~$V$ in general determine different Gödel

215:   logics~$\gdl{V}$ (sets of those formulas which evaluate to~$1$ in every

216:   interpretation into~$V$).  It is shown that $\gdl{V}$ is axiomatizable iff

217:   $V$ is finite, $V$ is uncountable with $0$ isolated in $V$, or every

218:   neighborhood of $0$ in $V$ is uncountable.  Complete axiomatizations for

219:   each of these cases are given.  The r.e. prenex, negation-free, and

220:   existential fragments of all first-order Gödel logics are also

221:   characterized.

222: \end{abstract}

223: \tableofcontents

224: 

225: 

226: \section{Introduction}

227: 

228: \subsection{Motivation}

229: 

230: The logics we investigate in this paper, first-order Gödel logics, can be

231: characterized in a rough-and-ready way as follows:  The language is a standard

232: first-order language.  The logics are many-valued, and the sets of truth

233: values considered are closed subsets of $[0, 1]$ which contain both~$0$

234: and~$1$. $1$ is the ``designated value,'' i.e., a formula is valid if

235: it receives the 

236: value~$1$ in every interpretation.  The truth functions of conjunction and

237: disjunction are minimum and maximum, respectively, and quantifiers are defined

238: by infimum and supremum over subsets of the set of truth values.  The

239: characteristic operator of Gödel logics, the Gödel conditional, is defined by

240: $a \limp b = 1$ if $a \le b$ and $= b$ if $a > b$.  Because the truth values

241: are ordered (indeed, in many cases, densely ordered), the semantics of Gödel

242: logics is suitable for formalization of \emph{comparisons}.  It is

243: related in this respect to a more widely known many-valued logic, \L

244: ukasiewicz (or ``fuzzy'') logic---yet the truth function of the \L ukasiewicz

245: conditional is defined not just using comparison, but also addition.  In

246: contrast to \L ukasiewicz logic, which might be considered a logic of

247: \emph{absolute} or \emph{metric comparison}, Gödel logics are logics of

248: \emph{relative comparison}.  This alone makes Gödel logics an interesting

249: subject for logical investigations.

250: 

251: There are other reasons why the study of Gödel logics is important.  As noted,

252: Gödel logics are related to other many-valued logics of recognized importance.

253: %such as \L ukasiewicz logic.  

254: Indeed, Gödel logic is one of the three basic

255: $t$-norm based logics which have received increasing attention in the last 15

256: or so years \cite{hajek} (the others are \L ukasiewicz and product logic).

257: Yet Gödel logic is also closely related to intuitionistic logic: it is the

258: logic of linearly-ordered Heyting algebras.  In the propositional case,

259: infinite-valued Gödel logic can be axiomatized by the intuitionistic

260: propositional calculus extended by the axiom schema $(A \limp B) \lor (B \limp

261: A)$.  This connection extends also to Kripke semantics for intuitionistic

262: logic: Gödel logics can also be characterized as logics of (classes of)

263: linearly ordered and countable intuitionistic Kripke structures with

264: constant domains \cite{BeckPrei05Kripke}.

265: 

266: One of the surprising facts about Gödel logics is that whereas there is

267: only one infinite-valued propositional Gödel logic, there are infinitely many

268: different infinite-valued first-order Gödel logics depending on the choice of

269: the set of truth values.  This is also the case when one considers the

270: propositional consequence relation, and likewise when the language is extended

271: to include quantification over propositions.  For both quantified

272: propositional and first-order Gödel logics, different sets of truth values

273: with different order-theoretic properties result in different sets of valid

274: formulas.  Hence it is necessary to consider truth value sets other than the

275: standard unit interval.

276: 

277: In the light of the result of Scarpellini \cite{scarpellini} on

278: non-axiomatizability of infinite-valued first-order \L ukasiewicz logic

279: which can be extended to almost all linearly ordered infinite-valued 

280: logics, it is also surprising that some infinite-valued Gödel logics are 

281: recursively enumerable. Our

282: main aim in this paper is to characterize those sets of truth values which

283: give rise to axiomatizable Gödel logics, and those whose sets of validities

284: are not r.e.  We show that a set $V$ of truth values determines an

285: axiomatizable first-order Gödel logic if, and only if, $V$ is finite, $V$ is

286: uncountable and $0$ is isolated, or every neighborhood of $0$ in $V$ is

287: uncountable.  These cases also determine different sets of validities: the

288: finite-valued Gödel logics $\Gn$, the logic $\Go$, and the ``standard''

289: infinite-valued Gödel logic~$\GR$ (based on the truth value set $[0, 1]$).

290: 

291: \subsection{History of Gödel logics}

292: 

293: Gödel logics are one of the oldest families of many-valued logics.

294: Propositional finite-valued Gödel logics were introduced by Gödel in

295: \cite{goedel33} to show that intuitionistic logic does not have a

296: characteristic finite matrix. They provide the first examples of intermediate

297: logics (intermediate, that is, in strength between classical and

298: intuitionistic logics).  Dummett \cite{dummett} was the first to study

299: infinite valued propositional Gödel logics, axiomatizing the set of

300: tautologies over infinite truth-value sets by intuitionistic logic extended by

301: the linearity axiom $(A \limp B) \lor (B \limp A)$. Hence, infinite-valued

302: propositional Gödel logic is also sometimes called Gödel-Dummett logic or

303: Dummett's \textsc{LC}. In terms of Kripke semantics, the characteristic

304: linearity axiom picks out those accessibility relations which are linear

305: orders.

306: 

307: Standard first-order Gödel logic~$\GR$---the one based on the full interval

308: $[0,1]$---has been discovered and studied by several people independently.

309: Alfred Horn was probably the first: He discussed this logic under the name

310: \emph{logic with truth values in a linearly ordered Heyting algebra}

311: \cite{horn}, and gave an axiomatization and the first completeness proof.

312: Takeuti and Titani~\cite{TT} called $\GR$ \emph{intuitionistic fuzzy logic},

313: and also gave an axiomatization for which they proved the completeness. This

314: system incorporates the density rule

315: \[ 

316: \infer{\Gamma\proves{A\lor (C\limp B)}}{\Gamma\proves{A\lor (C\limp p) \lor

317:     (p\limp B)}}

318: \]

319: (where~$p$ is any propositional variable not occurring in the lower sequent.)

320: The rule is redundant for an axiomatization of~$\GR$, as was shown by Takano

321: \cite{takano}, who gave a streamlined completeness proof of Takeuti-Titani's

322: system without the rule. (A syntactical proof of the elimination of the

323: density rule was later given in~\cite{BaazZach00CSL}.  Other proof-theoretic

324: investigations of Gödel logics can be found in \cite{BC02} and \cite{BFC03}.)

325: The density rule is nevertheless interesting: It forces the truth value set to

326: be dense in itself (in the sense that, if the truth value set isn't dense in

327: itself, the rule does not preserve validity).  This contrasts with the

328: expressive power of formulas: no formula is valid only for truth value sets

329: which are dense in themselves.

330: 

331: First-order Gödel logics other than $\GR$ were first considered in

332: \cite{BaazLeitschZach:96}, where it was shown that $\gdl{\vdn}$, based on the

333: truth value set $V_\vdn = \{1/k : k \in \N\} \cup \{0\}$ is not r.e.  Hájek

334:   \cite{Hajek05} has recently improved this result, and showed that not only

335:   is the set of validities not r.e., it is not even arithmetical.  Hájek

336:   also showed that the Gödel logic~$\gdl{\vup}$ based on $V_\vup =  \{1-1/k : k \in \N\}

337:     \cup \{1\}$ is $\Pi_2$-complete. Results preliminary to the results of the

338:     present paper were reported in \cite{BPZ03,Prei02LPAR,Prei03PHD}. 

339: 

340: \subsection{Overview of the results}

341: 

342: We begin with a preliminary discussion of the syntax and semantics of Gödel

343: logics, including a discussion of some of the more interesting special cases

344: of first-order Gödel logics and their relationships

345: (Section~\ref{sec:preliminaries}).  In Section~\ref{sec:order}, we

346: present some relevant results regarding the topology of truth-value

347: sets. 

348: 

349: The main results of the paper are contained in

350: Sections~\ref{sec:countable}--\ref{sec:finite}.  We provide a complete

351: classification of the axiomatizability of first order Gödel logics. The main

352: results are, that a logic based on a truth value set~$V$ is axiomatizable if

353: and only if

354: \begin{enumerate}

355: \item $V$ is finite (Section~\ref{sec:finite}), or 

356: \item $V$ is uncountable and $0$ is contained in the perfect kernel

357:   (Section~\ref{ssec:perfect}), or

358: \item $V$ is uncountable and $0$ is isolated (Section~\ref{ssec:isolated}).

359: \end{enumerate}

360: In all other cases, i.e., logics with countable truth value set

361: (Section~\ref{sec:countable}) and those where there is a countable

362: neighborhood of~$0$ and $0$ is not isolated (Section~\ref{sec:uncount-nonax}),

363: the respective logics are not r.e.

364: 

365: In Section~\ref{sec:fragments}, we investigate the complexity of fragments of

366: first-order Gödel logic, specifically, the prenex fragments

367: (Section~\ref{sec:prenex}), the $\bot$-free fragments

368: (Section~\ref{sec:botfree}), and the existential ($\forall$-free) fragments

369: (Section~\ref{sec:efrag}).  We show that the prenex fragment of a Gödel logic

370: is axiomatizable if and only if the truth value set is finite or uncountable.

371: This means that there are truth-value sets where the prenex fragment of the

372: corresponding logic is r.e. even though the full logic is not. Moreover, there

373: all axiomatizable prenex fragments coincide.  This is also the case for

374: $\bot$-free and existential fragments, but in these cases only those truth

375: value sets determine r.e. $\bot$-free and existential fragments for which also

376: the full logic is r.e., viz., truth value sets which are finite, uncountable

377: with $0$ isolated, and those where every neighborhood of $0$ is uncountable.

378: 

379: 

380: \section{Preliminaries}\label{sec:preliminaries}

381: 

382: \subsection{Syntax and Semantics}

383: 

384: In the following we fix a standard first-order language~$\LL$ with finitely or

385: countably many predicate symbols~$P$ and finitely or countably many function

386: symbols~$f$ for every finite arity~$k$.  In addition to the two quantifiers

387: $\forall $ and $\exists$ we use the connectives $\vee$, $\wedge$, $\to$ and

388: the constant $\bot$ (for `false'); other connectives are introduced as

389: abbreviations, in particular we let $\lnot A \equiv (A \to \bot)$.

390: 

391: Gödel logics are usually defined using the single truth value set~$[0,1]$. For

392: propositional logic the choice of any infinite subset of $[0,1]$ leads to the

393: same propositional logic (set of tautologies). In the first order case, where

394: quantifiers will be interpreted as infima and suprema, a closed subset of

395: $[0,1]$ is necessary.

396: 

397: \begin{definition}[Gödel set]

398:   A \emph{Gödel set} is a closed set~$V \subseteq [0,1]$

399:   which contains $0$ and~$1$.  

400: \end{definition}

401: 

402: The semantics of Gödel logics, with respect to a fixed Gödel set as truth

403: value set and a fixed language~$\LL$ of predicate logic, is defined using the

404: extended language $\LL^U$, where $U$ is the universe of the

405: interpretation~$\I$.  $\LL^U$ is $\LL$ extended with constant symbols for each

406: element of $U$.

407: 

408: \begin{definition}[Semantics of Gödel logic]\label{def:gsemantik}

409:   Fix a Gödel set $V$.

410:   An \emph{interpretation $\I$} into $V$ consists of 

411:   \begin{enumerate}

412:   \item  a nonempty set $U = U^\I$, the

413:     `universe' of $\I$, 

414:   \item  for each $k$-ary predicate symbol $P$, 

415:     a function $P^\I : U^k \to V$,

416:   \item for each $k$-ary function symbol $f$, a function

417:     $f^\I: U^k \to U$.

418:   \item for each variable~$v$, a value $v^\I \in U$.

419:   \end{enumerate}

420:   

421:   Given an interpretation $\I$, we can naturally define a value $t^\I$ for any

422:   term $t$ and a truth value $\I(A)$ for any formula $A$ of $\LL^U$. For a

423:   terms $t = f(u_1, \ldots, u_k)$ we define $\I(t)=f^\I(u_1^\I, \ldots,

424:   u_k^\I)$. For atomic formulas $A \equiv P(t_1,\dots, t_n)$, we define $\I(A)

425:   = P^\I(t_1^\I, \ldots, t_n^\I)$. For composite formulas $A$ we define

426:   $\I(A)$ by:

427:   \begin{align}

428:     \I(\bot) &= 0\\

429:     \I(A \land B) &= \min(\I(A),\I(B))\\

430:     \I(A \lor B) &= \max(\I(A),\I(B))\\

431:     \I(A \limp B) &= \begin{cases} 1 & \I(A)\le \I(B)\\

432:                                   \I(B) & \text{ otherwise}

433:                      \end{cases}\\

434:     \I(\qa x\, A(x)) &= \inf \{\I(A(u)) \suchthat u \in U\}\\

435:     \I(\qe x\, A(x)) &= \sup \{\I(A(u)) \suchthat u \in U\}

436:   \end{align}

437:   (Here we use the fact that every Gödel sets $V$ is a \emph{closed} subset of

438:   $[0,1]$ in order to be able to interpret $\forall$ and $\exists$ as $\inf$

439:   and $\sup$ in~$V$.)

440: 

441:   If $\I(A) = 1$, we say that $\I$ \emph{satisfies} $A$, and write $\I

442:   \entails A$.

443: \end{definition}

444: 

445: \begin{definition}[Gödel logics based on $V$]\label{def:goedellogics}

446:   For a Gödel set $V$ we define the {\em first order Gödel logic $\gdl V$} as

447:   the set of all formulas of $\LL$ such that $\I \entails A$ for all

448:   $V$-interpretations~$\I$.

449: \end{definition}

450: 

451: It should be noted that for Gödel logics with~$0$ isolated, the notion of 

452: \emph{satisfiability}

453: for sets of formulas is not particularly interesting, since a set of

454: formulas~$\Gamma$ is satisfiable (in the sense that there is an $\I$ so that

455: $\I \entails A$ for all $A \in \Gamma$) iff it is satisfiable classically.

456: \fxnote{$0$ nicht isoliert: $(\forall xP(x)\limp\bot)\land\forall x¬¬P(x)$ Gegenbsp!}

457: For this reason, we take \emph{entailment} to

458: be the fundamental model-theoretic notion.

459: 

460: \begin{definition}

461:   If $\Gamma$ is a set of formulas (possibly infinite), we say that $\Gamma$

462:   entails $A$ in $\gdl V$, $\Gamma \entails_V A$ iff for all $\I$ into $V$,

463:   \[ 

464:   \inf \{\I(B) : B \in \Gamma\} \le \I(A);

465:   \]

466:   and $\Gamma$ \emph{$1$-entails} $A$ in $\gdl V$, $\Gamma \Vdash_V A$, iff,

467:   for all~$\I$ into $V$, whenever $\I(B) = 1$ for all $B \in \Gamma$, then

468:   $\I(A) = 1$.

469: \end{definition}

470: 

471: \begin{notation}

472:   We will write $\Gamma \entails A$ instead of $\Gamma\entails_V A$ in

473:   case it is obvious which truth value set $V$ is meant. We will

474:   sometimes write $\Gamma \entails \Delta \in \gdl V$, by which we mean 

475:   that $\Gamma \entails_V \Delta$. The notation $\gdl V \entails A$

476:   stands for $\emptyset \entails_V A$, or $A \in \gdl V$. 

477: \end{notation}

478: 

479: Whether or not a formula $A$ evaluates to~1 under an interpretation~$\I$

480: depends only on the \emph{relative ordering} of the truth values of the atomic

481: formulas (in $\LL^\I$), and not directly on the set~$V$ or on the

482: \emph{values} of the atomic formulas. If $V \subseteq W$ are both Gödel sets,

483: and $\I$ is an interpretation into $V$, then $\I$ can be seen also as a

484: interpretation into $W$, and the values $\I(A)$, computed recursively using

485: (1)--(6), do not depend on whether we view $\I$ as a $V$-interpretation or a

486: $W$-interpretation.  Consequently, if $V \subseteq W$, there are more

487: interpretations into $W$ than into $V$.  Hence, if $\Gamma \entails_W A$ then

488: also $\Gamma \entails_V A$ and $\gdl{W} \subseteq \gdl{V}$.

489: 

490: This can be generalized to embeddings between Gödel sets other than inclusion.

491: First, we make precise which formulas are involved in the computation of the

492: truth-value of a formula~$A$ in an interpretation~$\I$:

493: 

494: \begin{definition}\label{def:subformula}

495:   The only subformula of an atomic formula $P$ in $\LL^U$ is  $P$

496:   itself. The subformulas of $A \star B$ for

497:   $\star \in \{\limp,\land,\lor\}$ are the subformulas of  $A$ and of

498:   $B$, together with $A \star B$ itself.  The subformulas of 

499:   $\qa x\,A(x)$ and $\qe x\,A(x)$ with respect to a universe $U$ are all

500:   subformulas of all $A(u)$ for $u\in U$, together with  $\qa x\,A(x)$

501:   (or, $\qe x\,A(x)$, respectively) itself.  

502: 

503:   The set of truth-values of subformulas of $A$ under a given

504:   interpretation~$\I$ is denoted by

505:   \[ \subval(\I,A) = \{ \I(B) \suchthat B 

506:   \text{ subformula of $A$ w.r.t.\ $U^\I$}\} \cup \{0,1\}

507:    \] 

508:    If $\Gamma$ is a set of formulas, then $\subval(\I, \Gamma) = \bigcup

509:    \{\subval(\I, A) : A \in \Gamma\}$.

510: \end{definition}

511: 

512: \begin{lemma}\label{lem:induced-interpretation}

513:   Let $\I$ be a $V$-interpretation, and let $h\colon \subval(\I, \Gamma) \to

514:   W$ be a mapping satisfying the following properties:

515: \begin{enumerate}

516: \item $h(0) = 0$, $h(1) = 1$;

517: \item $h$ is strictly monotonic, i.e., if $a < b$, then $h(a) < h(b)$;

518: \item for every $X \subseteq \subval(\I, \Gamma)$, $h(\inf X) = \inf h(X)$ and

519: $h(\sup X) = \sup h(X)$ (provided $\inf X$, $\sup X \in \subval(\I, \Gamma)$).

520: \end{enumerate}

521: Then the $W$-interpretation $\I_h$ 

522: with universe $U^\I$, $f^{\I_h} = f^\I$, and for atomic $B \in\LL^\I$,

523: \[

524:     \I_h(B) = \begin{cases} h(\I(B)) & \text{ if $\I(B) \in \dom h$} \\ 

525:                             1 &        \text{ otherwise}

526:                \end{cases}

527: \]

528: satisfies $\I_h(A) = h(\I(A))$ for all $A \in \Gamma$.

529: \end{lemma}

530: 

531: \begin{proof}

532:   By induction on the complexity of~$A$.  If $A \equiv \bot$, the claim

533:   follows from (1).  If $A$ is atomic, it follows from the definition of

534:   $\I_h$.  For the propositional connectives the claim follows from the strict

535:   monotonicity of~$h$ (2).  For the quantifiers, it follows from property~(3).

536: \end{proof}

537: 

538: \begin{remark}

539:   Note that the construction of $\I_h$ and the proof of

540:   Lemma~\ref{lem:induced-interpretation} also goes through without the

541:   condition $h(0) = 0$, provided that the formulas in $\Gamma$ do not

542:   contain~$\bot$, and goes through without the requirement that existing inf's

543:   be preserved ($h(\inf X) = \inf h(X)$ if $\inf X \in \subval(\I, \Gamma)$)

544:   provided they do not contain~$\forall$.

545: \end{remark}

546: 

547: \begin{definition}

548:   A \emph{\g-embedding} $h\colon V \to W$ is a strictly monotonic, continuous

549:   mapping between Gödel sets which preserves

550:   $0$ and $1$.

551: \end{definition}

552: 

553: \begin{lemma}\label{lem:g-embed}

554:   Suppose $h\colon V \to W$ is a \g-embedding. (a) If $\I$ is a

555:   $V$-interpretation, and $\I_h$ is the interpretation induced by $\I$ and

556:   $h$, then $\I_h(A) = h(\I(A))$. (b) If $\Gamma \entails_W A$ then $\Gamma

557:   \entails_V A$ (and hence $\gdl{W} \subseteq \gdl{V}$). (c) If $h$ is

558:   bijective, then $\Gamma \entails_W A$ iff $\Gamma \entails_V A$ (and hence,

559:   $\gdl{V} = \gdl{W}$).

560: \end{lemma}

561: 

562: \begin{proof}

563:   (a) $h$ satisfies the conditions of Lemma~\ref{lem:induced-interpretation},

564:   for $\Gamma$ the set of all formulas. (b) If $\Gamma \nentails_V A$, then

565:   for some $\I$, $\I(B) = 1$ for all $B \in \Gamma$ and $\I(A) < 1$.  By

566:   Lemma~\ref{lem:induced-interpretation}, $\I_h(B) = 1$ for all $B \in \Gamma$

567:   and $\I_h(A) < 1$ (by strict monotonicity of $h$). Thus $\Gamma \nentails_W

568:   A$. (c) If $h$ is bijective then $h^{-1}$ is also a \g-embedding.

569: \end{proof}

570: 

571: \begin{definition}[Submodel, elementary submodel]

572:   Let $\I_1$, $\I_2$ be interpretations.  We write $\I_1 \subseteq \I_2$ 

573:   ($\I_2$ extends $\I_1$) iff

574:   $U^{\I_1} \subseteq U^{\I_2}$, and for all $k$, all $k$-ary 

575:   predicate symbols $P$ in $\LL$, and all $k$-ary function symbols $f$

576:   in $\LL$ we have

577:   \[ P^{ \I_1 } =  P^{ \I_2 } \upharpoonright (U^{\I_1})^k  \quad

578:      f^{ \I_1 } =  f^{ \I_2 } \upharpoonright (U^{\I_1})^k  \quad

579:      \]

580:   or in other words, if $\I_1$ and $\I_2$ agree on closed atomic

581:   formulas.  

582: 

583:   We write $\I_1 \prec \I_2$ if $\I_1 \subseteq \I_2$ and $\I_1(A) = \I_2(A)$ 

584:   for all $\LL^{U^{\I_1}}$-formulas $A$. 

585: \end{definition}

586: 

587: \begin{proposition}[Downward Löwenheim-Skolem]\label{fact:loewenheim}

588:   For any interpretation $\I$ with $U^\I$ infinite, there is an

589:   interpretation $\I' \prec \I$  with a countable universe~$U^{\I'} $. 

590: \end{proposition}

591: 

592: \begin{proof}[Proof sketch]

593:   The proof is an easy generalization of the construction for the classical

594:   case.  We construct a sequence of countable subsets $U_1 \subseteq U_2

595:   \subseteq \cdots$ of $U^\I$: $U_1$ simply contains $t^\I$ for all closed

596:   terms of the original language.  $U_{i+1}$ is constructed from $U_i$ by

597:   adding, for each of the (countably many) formulas of the form $\exists x\,

598:   A(x)$ and $\forall x\, A(x)$ in the language $\LL^{U_i}$, a countable

599:   sequence $a_j$ of elements of $U^\I$ so that $(\I(A(a_j)))_j \to \I(\exists

600:   x\, A(x))$ or $\to \I(\forall x\, A(x))$, respectively.  $U^{\I'} =

601:   \bigcup_i U_i$.

602: \end{proof}

603: 

604: 

605: \begin{lemma}\label{lemma:interpretation-cut-off}

606:   Let $\I$ be a interpretation into $V$, $w\in[0,1]$, and let $\I_w$

607:   be defined by

608:   \[ \I_w(B) = \begin{cases} \I(B) &\text{ if $\I(B)<w$}\\

609:     1 &\text{ otherwise}

610:                 \end{cases}

611:   \]

612:   for atomic formulas $B$ in $\LL^U$.  Then $\I_w$ is an interpretation into

613:   $V$.  If $w \notin \subval(\I, A)$, then $\I_w(A) = \I(A)$ if $\I(A) < w$,

614:   and $\I_w(A) = 1$ otherwise.

615: \end{lemma}

616: 

617: \begin{proof}

618:   Let $h_w(a)=a$ if $a<w$ and $=1$ otherwise.  By induction on the complexity

619:   of formulas $B$ it is easily shown that $\I'(B)=h_w(\I(B))$ for all

620:   subformulas $B$ of $A$ w.r.t.\ $U^\I$.

621: \end{proof}

622: 

623: \begin{proposition}\label{prop:consequences}

624: $\Gamma \entails A$ iff $\Gamma \Vdash A$

625: \end{proposition}

626: 

627: \begin{proof}

628:   Only if: obvious. If: Suppose that $\Gamma \nentails A$, i.e., there is a

629:   $V$-interpretation $\I$ so that $\inf \{\I(B) : B \in \Gamma\} > \I(A)$.  By

630:   Proposition~\ref{fact:loewenheim}, we may assume that $U^\I$ is countable.

631:   Hence, there is some $w$ with $\I(A) < w < \inf\{\I(B) : B \in \Gamma\}$ and

632:   $w \notin \subval(\I, \Gamma \cup \{A\})$.  Let $\I_{w}$ be as in

633:   Lemma~\ref{lemma:interpretation-cut-off}.  Then $\I_w(B) = 1$ for all $B \in

634:   \Gamma$ and $\I_w(A) < 1$.

635: \end{proof}

636: 

637: The coincidence of the two consequence relations is a unique feature of Gödel

638: logics.  Proposition~\ref{prop:consequences} does not hold in \L ukasiewicz

639: logic, for instance. There, $A, A \limp_\textrm{\L} B \Vdash B$ but $A, A

640: \limp_\textrm{\L} B \nentails B$.  In what follows, we will use $\entails$

641: when semantic consequence is at issue; the preceding propositions shows that

642: the results we obtain for $\entails$ hold for $\Vdash$ as well.

643: 

644: \begin{lemma}[Semantic deduction theorem]\label{thm:semdeduc}

645:   \[ \Gamma, A \entails B \quad\text{iff}\qquad \Gamma\entails A\limp B.\]

646: \end{lemma}

647: 

648: \begin{proof}

649:   Immediate consequence of the definition of $\entails$ and the

650:   semantics for $\limp$.

651: \end{proof}

652: 

653: We want to conclude this part with two interesting observations:

654: 

655: \paragraph{Relation to residuated algebras}

656: If one considers the truth value set as a Heyting algebra with $a\wedge

657: b = \min(a,b)$,  $a\vee b = \max(a,b)$, and

658: \[ a \to b = \left\{

659:   \begin{array}{ll}

660:     1 & \mbox{if $a\le b$ }\\

661:     b & \mbox{otherwise}\\

662:   \end{array}\right.

663: \]

664: then $\to$ and $\wedge$ are residuated, i.e.,

665: \[ 

666:   (a \to b)  = \sup \{\, x: \, (x\wedge a)\, \le\, b\, \}. 

667: \]

668: 

669: \paragraph{The Gödel conditional}

670: A large class of many-valued logics can be developed from the theory of

671: $t$-norms \cite{hajek}. The class of $t$-norm based logics includes not only

672: (standard) Gödel logic, but also {\L}ukasiewicz- and product logic. In these

673: logics, the conditional is defined as the residuum of the respective $t$-norm,

674: and the logics differ only in the definition of their $t$-norm and the

675: respective residuum, i.e., the conditional. The truth function for the Gödel

676: conditional is of particular interest as it can be `deduced' from simple

677: properties of the evaluation and the entailment relation, a fact which was

678: first observed by G.~Takeuti.

679: \begin{lemma}\label{lemma:takeuti}

680:   Suppose we have a standard language containing a `conditional'

681:   $\twoheadrightarrow$ interpreted by a truth-function into $[0,1]$. Suppose

682:   further that 

683:   \begin{enumerate}

684:   \item a conditional evaluates to~$1$ if the truth value of the antecedent

685:     is less or equal to the truth value of the consequent, i.e.,

686:     if $\I(A) \le \I(B)$, then $\I(A \twoheadrightarrow B) = 1$;

687:   \item $\entails$ is defined as above, i.e., if $\Gamma \entails B$, then

688:     $\min \{ \I(A) \suchthat A\in\Gamma \} \le \I(B)$;

689:   \item the deduction theorem holds, i.e., $\Gamma \cup \{ A \} \entails B

690:     \dequiv \Gamma \entails A \twoheadrightarrow B$.

691:   \end{enumerate}

692:   Then $\twoheadrightarrow$ is the Gödel conditional.

693: \end{lemma}

694: 

695: \begin{proof}

696:   From (1), we have that $\I(A \twoheadrightarrow B) = 1$ if $\I(A) \le

697:   \I(B)$.  Since $\entails$ is reflexive, $B \entails B$. Since it is

698:   monotonic, $B, A \entails B$.  By the deduction theorem, $B \entails A

699:   \twoheadrightarrow B$.  By (2),

700:   \[ 

701:   \I(B) \le \I(A \twoheadrightarrow B).

702:   \]

703:   From $A \twoheadrightarrow B \entails A \twoheadrightarrow B$ and the

704:   deduction theorem, we get $A \twoheadrightarrow B, A \entails B$. By (2),

705:   \[ 

706:   \min \{\I(A \twoheadrightarrow B), \I(A)\} \le \I(B).

707:   \]

708:   Thus, if $\I(A) > \I(B)$, $\I(A \twoheadrightarrow B) \le \I(B)$.

709: \end{proof}

710: 

711: Note that all usual conditionals (Gödel, \L ukasiewicz, product conditionals)

712: satisfy condition (1).  So, in some sense, the Gödel conditional is the only

713: many-valued conditional which validates both directions of the deduction

714: theorem for $\entails$.  For instance, for the \L ukasiewicz conditional

715: $\limp_\textrm{\L}$ the right-to-left direction fails: $A \limp_\textrm{\L} B

716: \entails A \limp_\textrm{\L} B$, but $A \limp_\textrm{\L} B, A

717: \nentails B$. (With respect to $\Vdash$, the left-to-right direction of the

718: deduction theorem fails for $\limp_\textrm{\L}$.)

719: 

720: % In order theoretic language, this means that the maps $x\mapsto (a\wedge x)$

721: % and $y\mapsto (a\to y)$ are residuated.

722: 

723: 

724: \subsection{Axioms and deduction systems}

725: 

726: 

727: In this section we introduce certain axioms and deduction systems for

728: Gödel logics, and we will show completeness of these deduction systems

729: subsequently. We will use a Hilbert style proof system:

730: \begin{definition}

731:   A formula~$A$ is derivable from formulas $\Gamma$ in a system~$\cA$

732:   consisting of the axioms and the rules iff there are formulas $A_0$, \dots,

733:   $A_n = A$ such that for each $0 \le i \le n$ either $A_i \in \Gamma$, or

734:   $A_i$ is an instance of an axiom in $\cA$, or there are indices $j_1$,

735:   \dots, $j_l < i$ and a rule in $\cA$ such that $A_{j_1}$, \dots, $A_{j_l}$

736:   are the premises and $A_i$ is the conclusion of the rule. In this case we

737:   write $\Gamma \proves_{\cA} A$.

738: \end{definition}

739: 

740: We will denote by $\IL$ the following complete axiom system for intuitionistic

741: logic (taken from \cite{troelstra-handbook}). Rules are written as $A_1,

742: \ldots, A_n \proves A$.  \def\ax(#1){\hbox{({#1})}} 

743:   \fxnote{Besseres Axiomensystem mit weniger Regeln finden!}

744: \begin{align*}

745:   \ax(I1) &\quad A, A\limp B\proves B &

746:   \ax(I2) &\quad A\limp B,B\limp C\proves A\limp C\\

747:   \ax(I3) &\quad A\lor A\limp A, A\limp A\land A  &

748:   \ax(I4) &\quad A\limp A\lor B, A\land B\limp A\\

749:   \ax(I5) &\quad A\lor B\limp B\lor A, A\land B\limp B\land A &

750:   \ax(I6) &\quad A\limp B\proves C\lor A\limp C\lor B\\

751:   \ax(I7) &\quad A\land B\limp C \proves A\limp(B\limp C) &

752:   \ax(I8) &\quad A\limp (B\limp C) \proves A\land B\limp C\\

753:   \ax(I9) &\quad \bot\limp A \\

754:   \ax(I10) &\quad B^{(x)}\limp A(x) \proves B^{(x)}\limp\qa xA(x) &

755:   \ax(I11) &\quad \qa xA(x) \limp A(t)\\

756:   \ax(I12) &\quad A(t)\limp \qe xA(x) &

757:   \ax(I13) &\quad A(x)\limp B^{(x)} \proves \qe xA(x)\limp B^{(x)}

758: \intertext{(where $B^{(x)}$ means that $x$ is not free in $B$).}

759: \end{align*}

760: The following axioms will play an important r\^ole ($\axqs$ stands for

761: `quantifier shift', $\axlin$ for `linearity', $\axiso$ for `isolation

762: axiom of $0$', and $\axfinn$ for `finite with $n$ elements'):

763: \begin{align*}

764:   \axqs  &\quad \qa x(C^{(x)}\lor A(x)) \limp (C^{(x)}\lor\qa xA(x)) \\

765:   \axlin &\quad (A\limp B)\lor (B\limp A)\\

766:   \axiso &\quad \qa x\lnot\lnot A(x) \limp  \lnot\lnot\qa xA(x)\\

767:   \axfinn &\quad (\top\limp A_1) \lor (A_1\limp A_2)\lor \ldots \lor

768:     (A_{n-2}\limp A_{n-1})\lor (A_{n-1}\limp\bot)

769: \end{align*}

770: 

771: \begin{notation}

772:   $\H$ denotes the axiom system $\IL + \axqs + \axlin$.

773: 

774:   $\H_n$ for $n \ge 2$ denotes the axiom system $\H + \axfinn$.

775: 

776:   $\Ho$ denotes the axiom system $\H + \axiso$.

777: \end{notation}

778: 

779: \begin{theorem}[Soundness]\label{thm:soundness}

780:   Suppose $\Gamma$ contains only closed formulas, and all axioms of $\cA$ are

781:   valid in $\gdl{V}$. Then, if $\Gamma \proves_\cA A$ then $\Gamma \entails_V

782:   A$.

783: \end{theorem}

784: 

785: \begin{proof}

786:   By induction on the complexity of proofs.  By assumption, all axioms

787:   of~$\cA$ are valid in $\gdl{V}$, hence $\Gamma \entails_V A_i$ if $A_i$ is

788:   an axiom.  If $A_i \in \Gamma$, then obviously $\Gamma \entails_V A_i$. 

789:   It remains to show that the rules of inference preserve consequence.  We

790:   show this for modus ponens (I1) and existential generalization (I13), the

791:   other cases are analogous.

792: 

793:   Suppose $\Gamma \entails_V A$ and $\Gamma \entails_V A \limp B$ and consider

794:   a $V$-interpretation $\I$.  Let $v = \inf \{\I(C) : C \in \Gamma\}$.  If

795:   $\I(A) \le \I(B)$, then we have $v \le \I(B)$ because $v \le \I(A)$.  If

796:   $\I(A) > \I(B)$, then $v \le \I(B)$ because $\I(B) = \I(A \limp B)$.

797:   

798:   Suppose $\Gamma \entails_V A(x) \limp B$ and $x$ does not occur free in $B$.

799:   Let $\I$ be a $V$-interpretation, and let $w = \sup \{\I(A(u)) : u \in

800:   U^\I\}$, and let $\I_u$ be the interpretation resulting from $\I$ by

801:   assigning $u$ to $x$.  Since the formulas in $\Gamma$ are all closed and $B$

802:   does not contain $x$ free, $\I_u(C) = \I(C)$ for all $C \in \Gamma \cup

803:   \{B\}$ and $u \in U^\I$. Now suppose $w > \I(\exists x\, A(x) \limp B)$. In

804:   this case, $\I(\exists x\, A(x)) > \I(B)$.  But then, for some $u \in U^\I$,

805:   $\I_u(A(x)) > \I(B)$ and we'd have $w > \I_u(A(x) \limp B)$, contradicting

806:   $\Gamma \entails_V A(x) \limp B$.  The case for (I10) is analogous.

807: \end{proof}

808: 

809: Note that the restriction to closed formulas in $\Gamma$ is essential: $A(x)

810: \proves_\H \forall x\, A(x)$ but obviously $A(x) \nentails_V \forall x\,

811: A(x)$.

812: 

813: 

814: \subsection{Relationships between Gödel logics}\label{sec:intro:relgoedel}

815: 

816: The relationships between finite and infinite valued \emph{propositional}

817: Gödel logics are well understood.  Any choice of an infinite set of

818: truth-values results in the same propositional Gödel logic, viz., Dummett's

819: \LC.  \LC~was defined using the set of truth-values~$V_\dn$ (see below).

820: Furthermore, we know that \LC{} is the intersection of all finite-valued

821: propositional Gödel logics, and that it is axiomatized by intuitionistic

822: propositional logic~\IPL{} plus the schema $(A \impl B) \lor (B \impl A)$.

823: \IPL{} is contained in all Gödel logics.

824: 

825: In the first-order case, the relationships are somewhat more

826: interesting. First of all, let us note the following fact

827: corresponding to the end of the previous paragraph:

828: 

829: \begin{proposition}

830: Intuitionistic predicate logic~\IL{} is contained in all first-order

831: Gödel logics.

832: \end{proposition}

833: 

834: \begin{proof}

835: The axioms and rules of \IL{} are sound for the Gödel truth

836: functions.

837: \end{proof}

838: 

839: As a consequence of this proposition, we will be able to use any

840: intuitionistically sound rule and intuitionistically true formula

841: when working in any of the Gödel logics.

842: 

843: We can consider special truth value sets which will act as

844: prototypes for other logics. This is due to the fact that the logic is

845: defined extensionally as the set of formulas valid in this truth value

846: set, so the Gödel logics on different truth value sets may coincide.

847: \begin{align*}

848: V_\R & =  [0,1] \\

849: V_\vdn & =  \{1/k : k \ge 1\} \cup \{0\} \\

850: V_\vup & =  \{1 - 1/k : k \ge 1\} \cup \{1\} \\

851: V_m & = \{1 - 1/k : 1 \le k \le m-1\} \cup \{1\}

852: \end{align*}

853: The corresponding Gödel logics are $\gdl \R$, $\gdl \vdn$, $\gdl \vup$,

854: $\gdl m$. $\gdl \R$ is the \emph{standard} Gödel logic.

855: 

856: The logic $\gdl \vdn$ also turns out to be closely related 

857: to some temporal logics \cite{BaazLeitschZach:96,BaazLeitZach96TCS}.

858: $\gdl \vup$ is the intersection of all finite-valued first-order Gödel

859: logics as shown in Theorem~\ref{herbrand}.

860: 

861: \fxnote{Sollen die Ergebnisse dieses Abschnitts alle für $\entails_V$ statt für

862:   $\gdl V$ formuliert werden?}

863: 

864: \begin{proposition}

865: $\gdl \R = \bigcap_V \gdl V$, where $V$ ranges over all Gödel sets.

866: \end{proposition}

867: 

868: \begin{proof}

869: If $\gdl V \entails A$ for every $V$, then also for $V = [0, 1]$.  Conversely,

870: if there is some Gödel set $V$ and a $V$-interpretation $\I$ with $\I \nmodels

871: A$, then $\I$ is also a $[0,1]$-interpretation and hence $\gdl \R \nentails A$.

872: \end{proof}

873: 

874: \begin{proposition}\label{basic-cont}

875: The following strict containment relationships hold:

876: \begin{enumerate}

877: \item $\gdl m \supsetneq \gdl {m+1}$,

878: \item $\gdl m \supsetneq \gdl \vup \supsetneq \gdl \R$,

879: \item $\gdl m \supsetneq \gdl \vdn \supsetneq \gdl \R$.

880: \end{enumerate}

881: \end{proposition}

882: 

883: \begin{proof}

884: The only non-trivial part is proving that the containments are strict.

885: For this note that

886: \[

887: (A_1 \impl A_2) \lor \ldots \lor (A_m \impl A_{m+1})

888: \]

889: is valid in $\gdl m$ but not in $\gdl {m+1}$. Furthermore, let

890: \begin{align*}

891: C_\vup & =  \exists x(A(x) \impl \forall y\, A(y)) \mathrm{\ and} \\

892: C_\vdn & =  \exists x(\exists y\, A(y) \impl A(x)).

893: \end{align*}

894: $C_\dn$ is valid in all $\gdl m$ and in $\gdl \vup$ and $\gdl \dn$; $C_\vup$ is

895: valid in all $\gdl m$ and in $\gdl \vup$, but not in $\gdl \dn$; neither is

896: valid in $\gdl \R$ (\cite{BaazLeitschZach:96}, Corollary~2.9).

897: \end{proof}

898: 

899: The formulas $C_\vup$ and $C_\dn$ are of some importance in the study

900: of first-order infinite-valued Gödel logics.  $C_\vup$ expresses the

901: fact that every infimum in the set of truth values is a minimum, and

902: $C_\dn$ states that every supremum (except possibly $1$) is a maximum.

903: The intuitionistically admissible quantifier

904: shifting rules are given by the following implications and equivalences:

905: \[

906: \begin{array}{rcl}

907: (\forall x\, A(x) \land B) & \equiv & \forall x(A(x) \land B) \\

908: (\exists x\, A(x) \land B) & \equiv & \exists x(A(x) \land B) \\

909: (\forall x\, A(x) \lor B) & \impl & \forall x(A(x) \lor B) \\

910: (\exists x\, A(x) \lor B) & \equiv & \exists x(A(x) \lor B) \\

911: (B \impl \forall x\, A(x)) & \equiv & \forall x(B \impl A(x)) \\

912: (B \impl \exists x\, A(x)) & \rimpl & \exists x(B \impl A(x)) \\

913: (\forall x\, A(x) \impl B) & \rimpl & \exists x(A(x) \impl B) \\

914: (\exists x\, A(x) \impl B) & \equiv & \forall x(A(x) \impl B)

915: \end{array}

916: \]

917: The remaining three are:

918: \[

919: \begin{array}{rcl}

920: (\forall x\, A(x) \lor B) & \rimpl & \forall x(A(x) \lor B) \\

921: (B \impl \exists x\, A(x)) & \impl & \exists x(B \impl A(x)) \\

922: (\forall x\, A(x) \impl B) & \impl & \exists x(A(x) \impl B) 

923: \end{array}

924: \eqno{\begin{array}{r}(S_1)\\(S_2)\\(S_3)\end{array}}

925: \]

926: Of these, $S_1$ is valid in any Gödel logic.  $S_2$ and

927: $S_3$ imply and are implied by $C_\dn$ and $C_\vup$, respectively

928: (take $\exists y\, A(y)$ 

929: and $\forall y\, A(y)$, respectively, for $B$).  $S_2$ and $S_3$ are,

930: respectively, both valid in $\gdl \vup$, invalid and valid in $\gdl \dn$, and

931: both invalid in $\gdl \R$. Thus we obtain

932: \begin{corollary}

933:   $\gdl \vup$ is the only Gödel logic where every formula is equivalent to

934:   a prenex formula with the same propositional matrix.

935: \end{corollary}

936: 

937: We now also know that $\gdl \vup \neq \gdl \dn$.  In fact, we have

938: $\gdl \dn \subsetneq \gdl \vup$; this follows from the following theorem.

939: 

940: \begin{theorem}\label{herbrand}

941: \[\gdl \vup = \bigcap\limits_{m \ge 2} \gdl m\]

942: \end{theorem}

943: 

944: \begin{proof}

945:   By Proposition~\ref{basic-cont}, 

946:   $\gdl \vup \subseteq \bigcap_{m \ge 2}\gdl m$.  We now prove the reverse

947:   inclusion. Assume that there is an interpretation $\I$ such that

948:   $\I\nmodels A$, we want to give an interpretation $\I'$ such that

949:   $\I'\nmodels A$ and $\I'$ is a $\gdl m$ interpretation for

950:   some~$m$.

951:   

952:   Suppose there is an interpretation $\I$ such that $\I\nmodels A$, let $\I(A)

953:   = 1 - 1/k$. Let $w$ be somewhere between $1-1/k$ and $1-1/(k+1)$. Then the

954:   interpretation $\I_w$ given in Lemma~\ref{lemma:interpretation-cut-off} also

955:   is a counterexample for $A$.  Since there are only finitely many truth

956:   values below $w$ in $V_\vup$, $\I_w$ is a $\gdl {k+1}$ interpretation with

957:   $\I_w \nmodels A$. This completes the proof of the theorem.

958: \end{proof}

959: 

960: \begin{corollary}

961: $\gdl m \supsetneq \bigcap_m  \gdl m = 

962:    \gdl \vup \supsetneq \gdl \dn \supsetneq \gdl \R$

963: \end{corollary}

964: 

965: As we will see later, the axioms $\axfinn$ axiomatize exactly the

966: finite-valued Gödel logics. In these logics the quantifier shift axiom $\axqs$

967: is not necessary. Furthermore, all quantifier shift rules are valid in the

968: finite valued logics. Since $\gdl \vup$ is the intersection of all the finite

969: ones, all quantifier shift rules are valid in~$\gdl \vup$.  Moreover, any

970: infinite-valued Gödel logic other than $\gdl \vup$ is defined by some~$V$ which

971: either contains an infimum which is not a minimum, or a supremum (other

972: than~$1$) which is not a maximum.  Hence, in $V$ either $C_\vup$ or $C_\vdn$

973: will be invalid, and therewith either $S_3$ or $S_2$. We have:

974: 

975: \begin{corollary}

976:   $\gdl \vup$ is the only Gödel logic with infinite truth value set which

977:   admits all quantifier shift rules.

978: \end{corollary}

979: 

980: 

981: 

982: \section{Topology and Order}\label{sec:order}

983: 

984: 

985: %

986: % PERFECT SETS

987: %

988: \subsection{Perfect sets}

989: 

990: All the following notations, lemmas, theorems are carried out within the

991: framework of Polish spaces, which are separable, completely metrizable

992: topological spaces. For our discussion it is only necessary to know

993: that~$\bbR$ and all its closed subsets are Polish spaces (hence, every Gödel

994: set is a Polish space). For a detailed exposition see

995: \cite{Moschovakis:1980,kechris}.

996: 

997: \begin{definition}[limit point, perfect space, perfect set]

998:         \hskip0pt plus3pt minus 3pt

999:   A \emph{limit point} of a topological space is a point that is not

1000:   isolated, i.e.\ for every open neighborhood~$U$ of~$x$ there is a

1001:   point~$y\in U$ with~$y\neq x$. A space is \emph{perfect} if all its

1002:   points are limit points. A set $P\subseteq \bbR$ is \emph{perfect}

1003:   if it is closed and together with the topology induced from $\bbR$

1004:   is a perfect space.

1005: \end{definition}

1006: 

1007: It is obvious that all (non-trivial) closed intervals are perfect sets, also

1008: all countable unions of (non-trivial) intervals. But all these sets generated

1009: from closed intervals have the property that they are `everywhere dense',

1010: i.e., contained in the closure of their inner component. There is another very

1011: famous set which is perfect but is nowhere dense, the Cantor set:

1012: 

1013: \begin{example}[Cantor Set]

1014:   The set of all numbers in the unit interval which can be expressed in

1015:   triadic notation only by digits~$0$ and~$2$ is called \emph{Cantor

1016:     set}~$\bbD$.

1017: \end{example}

1018: 

1019: A more intuitive way to obtain this set is to start with the unit

1020: interval, take out the open middle third and restart this process with

1021: the lower and the upper third. Repeating this you get exactly the

1022: Cantor set because the middle third always contains the numbers which

1023: contain the digit $1$ in their triadic notation.

1024: 

1025: This set has a lot of interesting properties, the most important one

1026: is that it is a perfect set:

1027: 

1028: \begin{proposition}

1029:   The Cantor set is perfect.

1030: \end{proposition}

1031: 

1032: It is possible to embed the Cauchy space into any perfect space, yielding

1033: the following proposition:

1034: 

1035: \begin{proposition}\label{lem:uncountable}

1036:   If~$X$ is a nonempty perfect Polish space, then the cardinality

1037:   of~$X$ is~$2^{\alepho}$ and therefore, all nonempty perfect subsets,

1038:   too, have cardinality of the continuum.

1039: \end{proposition}

1040: 

1041: It is possible to obtain the following characterization of perfect

1042: sets (see \cite{winkler:howmuch}):

1043: 

1044: \begin{proposition}[Characterization of perfect sets in $\bbR$]\label{prop:winkler}

1045:   For any perfect subset of $\bbR$ there is a unique partition of the

1046:   real line into countably many intervals such that the intersections

1047:   of the perfect set with these intervals are either empty, the full

1048:   interval or isomorphic to the Cantor set.

1049: \end{proposition}

1050: 

1051: So we see that intervals and Cantor sets are prototypical for perfect

1052: sets and the basic building blocks of more complex perfect sets.

1053: 

1054: Every Polish space can be partitioned into a perfect kernel and a

1055: countable rest. This is the well known Cantor-Bendixon Theorem:

1056: 

1057: % \begin{definition}[condensation point]

1058: %   A point~$x$ in a topological space $X$ is a \emph{condensation

1059: %   point} if every open neighborhood of~$x$ is uncountable.

1060: % \end{definition}

1061: % 

1062: % Note that the condition for limit point is that every open

1063: % neighborhood is infinite, but not necessarily uncountable.

1064: 

1065: \begin{theorem}[Cantor-Bendixon]\label{thm:cantorbendixon}

1066:   Let~$X$ be a Polish space. Then~$X$ can be uniquely written as $X =

1067:   P \cup C$, with~$P$ a perfect subset of~$X$ and~$C$ countable and

1068:   open. The subset~$P$ is called the \emph{perfect kernel} of~$X$

1069:   (denoted with $V^\infty$).

1070: \end{theorem}

1071: 

1072: As a corollary we obtain that any uncountable Polish space contains a

1073: perfect set, and therefore, has cardinality~$2^{\alepho}$.

1074: 

1075: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1076: %

1077: % auskommentiert

1078: %

1079: %

1080: % CANTOR-BENDIXON DERIVATIVES AND RANKS

1081: %

1082: % \subsection{Cantor-Bendixon derivatives and ranks}

1083: % 

1084: % \begin{definition}[(iterated) Cantor-Bendixon derivative]

1085: %   \hskip0pt plus 5pt minus0pt

1086: %   For any topological space~$X$ let

1087: %   \[ X' = \{ x\in X \suchthat \mbox{$x$ is limit point of $X$}\}.\]

1088: %   We call~$X'$ the \emph{Cantor-Bendixon derivative} of~$X$.

1089: % 

1090: %   Using transfinite recursion we define the \emph{iterated

1091: %   Cantor-Bendixon derivatives}~$X^\alpha$, $\alpha$ ordinal, as

1092: %   follows:

1093: %   \begin{align*}

1094: %     X^0 & =  X\\

1095: %     X^{\alpha + 1} & =  (X^\alpha)'\\

1096: %     X^\lambda & =  \bigcap_{\alpha<\lambda} X^\alpha,

1097: %     \mbox{if~$\lambda$ is limit ordinal}.

1098: %   \end{align*}

1099: % \end{definition}

1100: % 

1101: % It is obvious that~$X'$ is closed, that $X$ is perfect iff~$X=X'$, and

1102: % that $(X^\alpha)$ for $\alpha$ ordinal is a decreasing transfinite

1103: % sequence of closed subsets of~$X$.

1104: % 

1105: % \begin{theorem}

1106: %   Let~$X$ be a Polish space. For some countable ordinal~$\alpha_0$,

1107: %   $X^\alpha = X^{\alpha_0}$ for all~$\alpha\ge\alpha_0$ and

1108: %   $X^{\alpha_0}$ is the perfect kernel of~$X$.

1109: % \end{theorem}

1110: % 

1111: % Thus, it is possible to obtain the perfect kernel in a more

1112: % constructive way. This leads to the definition of the Cantor-Bendixon

1113: % rank:

1114: % 

1115: % \begin{definition}[Cantor-Bendixon rank]

1116: %   For any Polish space~$X$, the least ordinal~$\alpha_0$ as above is

1117: %   called the \emph{Cantor-Bendixon rank} of~$X$ and is denoted

1118: %   by~$\cbrank X$. We will denote the perfect kernel of~$X$ with

1119: %   $X^\infty$ or $X^{\cbrank X}$.

1120: % \end{definition}

1121: % 

1122: % 

1123: % %

1124: % % COUNTABLE SETS

1125: % %

1126: % \subsection{The structure of countable compact topological spaces}

1127: % 

1128: % If the space~$X$ is countable then~$X^\infty = \emptyset$, since

1129: % every non-empty perfect set has at least cardinality of the continuum.

1130: % Now it is possible to give a finer characterization of these countable

1131: % sets by analyzing their structure under the Cantor-Bendixon derivatives. 

1132: % 

1133: % \begin{definition}[rank of an element, topological type of~$X$]

1134: % Let $X$ be a countable topological space. For any~$x\in X$, we can

1135: % define its (Cantor-Bendixon-)rank 

1136: % \[ \rg(x) = \sup \{ \alpha \suchthat x \in X^\alpha \}.\]

1137: % Thus, we also can define the rank of~$X$ equivalently by

1138: % \[ \cbrank X = \sup \{ \rg(x) \suchthat x\in X\}.\]

1139: % We call

1140: % \[\tau (X) = (\alpha, n),\quad \mbox{with } 

1141: %   \alpha = \alpha(X) = \cbrank X, \quad 

1142: %   n = n(X) = |X^{\cbrank X}|\]

1143: % the \emph{topological type} of~$X$.

1144: % \end{definition}

1145: % 

1146: 

1147: \subsection{Relation to Gödel logics}

1148: 

1149: 

1150: %\begin{lemma}\label{lemma:countable-into-cantor}

1151: %  Assume that $M\subset \bbR$ is a countable set and $P$ a perfect

1152: %  set. Then there is a \g-embedding from

1153: %  $M$ into $P$. 

1154: %\end{lemma}

1155: 

1156: The following lemma was originally proved in \cite{Prei03PHD}, where it was

1157: used to extend the proof of recursive axiomatizability of `standard' Gödel

1158: logics (those with $V=[0,1]$) to Gödel logics with a truth value set

1159: containing a perfect set in the general case. The following more

1160: simple proof is inspired by \cite{bgp}:

1161: 

1162: %\begin{proof}

1163: %Since there are uncountable many disjoint sets of the form 

1164: %$\bbQ - x :=\{q-x: q\in \bbQ\}$,

1165: %there is some $x$ such that $M\cap (\bbQ -x) = \emptyset$, so 

1166: %also $(M+x)\cap \bbQ=\emptyset$. 

1167: %So we may assume 

1168: %%%% (by translating $M$, if necessary)

1169: %that $M\cap \bbQ=\emptyset$.    

1170: %We may also assume $M\subseteq [0,1]$. 

1171: 

1172: %Since $P$ is perfect, we can find an \g-embedding $c$ from the Cantor

1173: %set $C\subseteq [0,1]$ into $P$.    

1174: 

1175: %Let $i$ be the natural bijection from $2^\omega$ (the set of infinite

1176: %$\{0,1\}$-sequences, ordered lexicographically) onto $C$.   $i$ 

1177: %is an order preserving homeomorphism. 

1178: 

1179: %For every $m\in M$ let $w(m)\in 2^\omega$ be the binary 

1180: %representation of $m$. Since $M$ does not contain any 

1181: %dyadic rational numbers, this representation is unique;  moreover,

1182: %the map $w$ is a \g-embedding.   

1183: %Now $c\circ i \circ w$ is also a \g-embedding from $M$ into $P$. 

1184: %\[ M  \pfeil{w}  2^\omega \pfeil{i} C  \pfeil{c} P \]

1185: 

1186: \begin{lemma}\label{lemma:countable-into-cantor}

1187:   Suppose that $M \subseteq [0,1]$ is countable and $P \subseteq [0,1]$ is

1188:   perfect. Then there is a strictly monotone continuous map 

1189:   $h\colon M \to  P$ (i.e., infima and suprema already existing in $M$

1190:   are preserved). Furthermore, if $\inf M \in M$, then one can choose

1191:   $h$ such that $h(\inf M) = \inf P$.

1192: \end{lemma}

1193: 

1194: \begin{proof}

1195:   Let $\sigma$ be the mapping which scales and shifts $M$ into $[0,1]$,

1196:   i.e.\ the mapping $x\to (x-\inf M)/(\sup M-\inf M)$ (assuming that

1197:   $M$ contains more than one point).

1198:   Let $w$ be an injective monotone map from $\sigma(M)$ into $2^\omega$,

1199:   i.e. $w(m)$ is a fixed binary representation of $m$. For dyadic rational

1200:   numbers (i.e.\ those with different binary representations) we fix one

1201:   possible.

1202:   

1203:   Let $i$ be the natural bijection from $2^\omega$ (the set of infinite

1204:   $\{0,1\}$-sequences, ordered lexicographically) onto $\bbD$, the Cantor set.

1205:   $i$ is an order preserving homeomorphism.  Since $P$ is perfect, we can find

1206:   a continuous strictly monotone map $c$ from the Cantor set $\bbD \subseteq

1207:   [0,1]$ into $P$, and $c$ can be chosen so that $c(0) = \inf P$.

1208:   

1209:   Now $h = c \circ i \circ w \circ \sigma$ is also a strictly monotone

1210:   map from $M$ into~$P$, and $h(\inf M) = \inf P$,  if $\inf M \in M$.

1211:   Since $c$ is continuous, existing infima and suprema are preserved.

1212: \end{proof}

1213: 

1214: \begin{corollary}\label{bendixon}

1215:   A Gödel set~$V$ is uncountable iff it contains a non-trivial dense

1216:   linear subordering.

1217: \end{corollary}

1218: 

1219: \begin{proof}

1220:   If: Every countable non-trivial dense linear order has order type

1221:   $\boeta$, $\one+\boeta$, $\boeta+\one$, or $\one+\boeta+\one$

1222:   \cite[Corollary~2.9]{rosenstein}, where $\boeta$ is the order type

1223:   of $\bbQ$.  The completion of any ordering of order type~$\boeta$

1224:   has order type~$\lambda$, the order type of $\bbR$

1225:   \cite[Theorem~2.30]{rosenstein}, thus the truth value set must be

1226:   uncountable.

1227:   

1228:   Only if: By Theorem~\ref{thm:cantorbendixon}, $V^\infty$ is non-empty. Take

1229:   $M = \bbQ \cap [0, 1]$ and $P = V^\infty$ in

1230:   Lemma~\ref{lemma:countable-into-cantor}.  The image of $M$ under~$h$ is a

1231:   non-trivial dense linear subordering in~$V$.

1232: \end{proof}

1233: 

1234: % \begin{proof}

1235: %   Only if: We define a dense linear subordering for any uncountable

1236: %   set. In fact we will give a dense linear subordering of the perfect

1237: %   kernel.

1238: 

1239: %   Since every perfect subset of the real line is a union of intervals

1240: %   and sets isomorphic to the Cantor set (Proposition~\ref{perfect}),

1241: %   it suffices to show the claim for those sets. For intervals the

1242: %   claim is trivial. Now consider the border points in a Cantor set,

1243: %   i.e., points which can only be approximated within the Cantor set

1244: %   from above or below but not both.  In the ternary notation these are

1245: %   the points with a finite number of~0 or a finite number of~2, i.e.,

1246: %   their ternary expansions are either $a=0.a_1a_2\ldots a_n$ or

1247: %   $b=0.b_1b_2\ldots b_n2222\ldots$ Each border point can be

1248: %   approximated by a sequence of inner points~$a^k$. For the $k$-th

1249: %   sequence element approximating a border point~$a$ we get $a^k$

1250: %   by appending $2k$~zeros and then a sequence of~$020202\ldots$ at the end

1251: %   ($a^k = 0.a_1\ldots a_n(00)^k\overline{02}$).  For the $k$-th

1252: %   sequence element approximating a border point~$b$ we define an

1253: %   approximating sequence $b^k$ by replacing the ternary expansion

1254: %   starting from the~$2k$-th 2 with a sequence of 02's ($b^k =

1255: %   0.b_1\ldots b_n(22)^k\overline{02}$).  The set of approximations of

1256: %   all border points is a dense subset: If $a^k = 0.a_1\ldots

1257: %   a_n(00)^{k}\overline{02}$ and $a^{k+1} = 0.a_1\ldots

1258: %   a_n(00)^{k}00\overline{02}$ are adjacent points in the sequence,

1259: %   then $a' = 0.a_1\ldots a_n(00)^{k}00022222\ldots$ is a border point

1260: %   with $a^{k+1} < a' < a^k$, hence there are infinitely many points

1261: %   $a'^\ell$ between~$a^k$ and~$a^{k+1}$ in the subset. Similarly for

1262: %   adjacent elements of a $b$-sequence. The set of border points is

1263: %   countable, therefore the set containing all the approximation

1264: %   sequences is countable and has all the necessary properties.

1265: % \end{proof}

1266: 

1267: % Note that for example 1/3 and 2/3 would not be in the dense linear

1268: % subordering, because between them there is no point of the perfect

1269: % set. We would replace 1/3 by a sequence of inner points approximating

1270: % 1/3 from below and replace 2/3 by a sequence of inner points

1271: % approximating 2/3 from above.

1272: 

1273: \begin{theorem}\label{thm:gs-id}

1274:   Suppose $V$ is a truth value set with non-empty perfect kernel $P$, and

1275:   let $W = V \cup [\inf P,1]$. Then 

1276:   $\mathnormal{\entails_V} = \mathnormal{\entails_W}$, i.e.\

1277:   $\Gamma \entails_V A$ iff $\Gamma \entails_W A$. Thus also the logics

1278:   induced by $V$ and $W$ are the same, i.e., $\gdl{V} = \gdl{W}$.

1279: \end{theorem}

1280: 

1281: \begin{proof}

1282:   As $V \subseteq W$ we have 

1283:   $\mathnormal{\entails_W} \subseteq \mathnormal{\entails_V}$ 

1284:   (cf.\ the Remark preceding Definition~\ref{def:goedellogics}).

1285:   Now assume that $\I$ is a $W$-interpretation which shows that

1286:   $\Gamma\entails_W A$ does \emph{not} hold, i.e.,

1287:   $\inf\{\I(B)\suchthat B\in\Gamma\} > \I(A)$. By

1288:   Proposition~\ref{fact:loewenheim}, we may assume that $U^\I$ is countable.

1289:   The set $\subval(\I, \Gamma\cup A)$ has cardinality at most

1290:   $\aleph_0$, thus there is a $b \in [0, 1]$ such that 

1291:   $b \notin \subval(\I, \Gamma\cup A)$ and $\I(A) < b < 1$.  By 

1292:   Lemma~\ref{lemma:interpretation-cut-off}, $\I_b(A) < b < 1$.  Now consider

1293:   $M = \subval(\I_b, \Gamma\cup A)$: these are all the truth values

1294:   from $W = V \cup [\inf P, 1]$ required to compute $\I_b(A)$ and

1295:   $\I_b(B)$ for all $B\in\Gamma$.  We have to find some way to map

1296:   them to $V$ so that the induced interpretation is a counterexample

1297:   to~$\Gamma\entails_V A$.  

1298: 

1299:   Let $M_0 = M \cap [0, \inf P)$ and 

1300:   $M_1 = (M \cap [\inf P, b])\cup\{\inf P\}$.

1301:   % Then $M = M_0 \cup M_1 \cup \{1\}$. 

1302:   By Lemma~\ref{lemma:countable-into-cantor} there is a strictly monotone

1303:   continuous (i.e. preserving all existing infima and suprema) map~$h$

1304:   from $M_1$ into $P$. Furthermore, we can choose~$h$ such that

1305:   $h(\inf M_1) = \inf P$.

1306: 

1307:   We define a function $g$ from $\subval(\I_b,\Gamma\cup A)$ to $V$ as

1308:   follows:

1309:   \[

1310:      g(x) = \begin{cases}

1311:                x          & 0\le x \le\inf P\\

1312:                h(x)       & \inf P \le x \le b\\

1313:                1          & x = 1

1314:             \end{cases}

1315:   \]

1316:   Note that there is no $x\in\subval(\I_b,\Gamma\cup A)$ with $b<x<1$.

1317:   This function has the following properties: $g(0)=0$, $g(1)=1$, $g$

1318:   is strictly monotonic and preserves existing infima and

1319:   suprema. Using Lemma~\ref{lem:induced-interpretation} we obtain that

1320:   $\I_g$ is a $V$-interpretation with $\I_g(C) = g(\I_b(C))$ for all

1321:   $C\in\Gamma\cup A$, thus also 

1322:   $\inf\{\I_g(B)\suchthat B\in\Gamma\} > \I_g(A)$.

1323: \end{proof}

1324: 

1325: 

1326: \section{Countable Gödel sets}\label{sec:countable}

1327: 

1328: In this section we show that the first-order Gödel logics where the set of

1329: truth values does not contain a dense subset are not axiomatizable. We

1330: establish this result by reducing the classical validity of a formula in all

1331: finite models to the validity of a formula in Gödel logic (the set of these

1332: formulas is not r.e.\ by Trakhtenbrot's Theorem).

1333: 

1334: \begin{definition}

1335:   A formula is called \emph{crisp} if all occurrences of atomic

1336:   formulas are either negated or double-negated.

1337: \end{definition}

1338: 

1339: \begin{lemma}\label{lm:crisp} If $A$ and $B$ are crisp and classically

1340:   equivalent, then also $\GR \models A \leftrightarrow B$. Specifically,

1341:   if $A(x)$ and $B$ are crisp, then

1342:   \begin{align*}

1343:     & \entails \qa xA(x)\limp B \leftrightarrow

1344:     \qe x(A(x)\limp B) \quad\text{and} \\

1345:     & \entails B\limp \qe xA(x) \leftrightarrow

1346:     \qe x(B\limp A(x)).

1347:   \end{align*}

1348: \end{lemma}

1349: 

1350: \begin{proof}

1351:   Given an interpretation~$\I$, define $\I'(C) = 1$ if $\I(C) > 0$ and $= 0$

1352:   if $\I(C) = 0$ for atomic~$C$.  It is easily seen that if $A$, $B$ are

1353:   crisp, then $\I(A) = \I'(A)$ and $\I(B) = \I'(B)$.  But $\I'$ is a classical

1354:   interpretation, so by assumption $\I'(A) = \I'(B)$.

1355: \end{proof}

1356: 

1357: 

1358: \begin{theorem}\label{thm:count-nonax}

1359:   If $V$ is countably infinite, then $\gdl V$ is not recursively

1360:   enumerable. 

1361: \end{theorem}

1362: 

1363: \begin{proof}

1364: By Theorem~\ref{bendixon}, $V$ is countably infinite iff it is

1365: infinite and does not contain a non-trivial densely ordered subset.

1366: We show that for every sentence $A$ there is a sentence $A^g$

1367: s.t. $A^g$ is valid in $\gdl V$ iff $A$ is true in every finite

1368: (classical) first-order structure.

1369: 

1370: We define $A^g$ as follows: Let $P$ be a unary and $L$ be a binary

1371: predicate symbol not occurring in~$A$ and let $Q_1$, \dots, $Q_n$ be

1372: all the predicate symbols in~$A$.  We use the abbreviations $x \in y

1373: \equiv \neg\neg L(x, y)$ and $x \prec y \equiv (P(y) \impl P(x)) \impl

1374: P(y)$.  Note that for any interpretation~\I, $\I(x \in y)$ is either

1375: $0$ or $1$, and as long as $\I(P(x)) < 1$ for all $x$ (in particular,

1376: if $\I(\exists z\, P(z)) < 1$), we have $\I(x \prec y) = 1$ iff

1377: $\I(P(x)) < \I(P(y))$.  Let $A^g \equiv$

1378: \begin{equation}\label{fm:countable}

1379:   \left\{

1380:     \begin{array}{l}

1381:       S \land {} c_1 \in 0 \land {} c_2 \in 0 \land 

1382:       c_2 \prec c_1 \land {}\\

1383:       \quad \forall i\bigl[\forall x, y \forall j \forall k \exists z\, D

1384:       \lor \forall x\neg(x \in s(i))\bigr]

1385:     \end{array}\right\}

1386:   \impl (A' \lor \exists u\, P(u))

1387: \end{equation}

1388: where $S$ is the conjunction of the standard axioms for $0$, successor

1389: and $\le$, with double negations in front of atomic formulas,

1390: \[ D\equiv \begin{array}{l}

1391: (j \le i \land x \in j \land k\le i \land y \in k \land x \prec y) \impl {}\\

1392: \qquad \impl (z \in s(i) \land x \prec z \land z \prec y)

1393: \end{array}\]

1394: and

1395: $A'$ is $A$ where every atomic formula is replaced by its double

1396: negation, and all quantifiers are relativized to the predicate

1397: $R(i)\equiv \exists x(x \in i)$.

1398: 

1399: Intuitively, $L$ is a predicate that divides a subset of the domain

1400: into levels, and $x \in i$ means that $x$ is an element of level~$i$.

1401: If the antecendent is true, then the true standard axioms~$S$ force

1402: the domain to be a model of PA, which could be either a standard model

1403: (isomorphic to $\bbN$) or a non-standard model ($\bbN$ followed by copies

1404: of $\bbZ$).

1405: $P$ orders the elements of the domain which fall into one of the

1406: levels in a subordering of the truth values.  

1407: 

1408: The idea is that for any

1409: two elements in a level $\le i$ there is an element in a not-empty

1410: level $j\ge i$

1411: which lies strictly between those two elements in the ordering given

1412: by~$\prec$.  If this condition cannot be satisfied, the levels above

1413: $i$ are empty.  Clearly, this condition can be satisfied in an

1414: interpretation~\I{} only for finitely many levels if $V$ does not

1415: contain a dense subset, since if more than finitely many levels are

1416: non-empty, then $\bigcup_{i} \{\I(P(d)) : \I \models d \in i\}$ gives

1417: a dense subset.  By relativizing the quantifiers in $A$ to the indices

1418: of non-empty levels, we in effect relativize to a finite subset of the

1419: domain.  We make this more precise:

1420: 

1421: Suppose $A$ is classically false in some finite structure~\I.  W.l.o.g. we may

1422: assume that the domain of this structure is the naturals $0$, \dots, $n$.  We

1423: extend $\I$ to a $\gdl V$-interpretation $\I^g$ with domain $\N$ as follows:

1424: Since $V$ contains infinitely many values, we can choose $c_1$, $c_2$, $L$ and

1425: $P$ so that $\exists x(x \in i)$ is true for $i = 0$, \dots, $n$ and false

1426: otherwise, and so that $\I^g(\exists x\, P(x)) < 1$.  The number-theoretic

1427: symbols receive their natural interpretation.  The antecedent of $A^g$ clearly

1428: receives the value~$1$, and the consequent receives $\I_g(\exists x\, P(x)) <

1429: 1$, so $\I^g \nmodels A^g$.

1430: 

1431: Now suppose that $\I \nmodels A^g$.  Then $\I(\exists x\, P(x)) < 1$.  In this

1432: case, $\I(x \prec y) = 1$ iff $\I(P(x)) < \I(P(y))$, so $\prec$ defines a

1433: strict order on the domain of $\I$.  It is easily seen that in order for the

1434: value of the antecedent of $A^g$ under \I{} to be greater than that of the

1435: consequent, it must be $= 1$ (the values of all subformulas are either $\le

1436: \I(\exists x\, P(x))$ or $= 1$).  For this to happen, of course, what the

1437: antecedent is intended to express must actually be true in~$\I$, i.e., that $x

1438: \in i$ defines a series of levels and any level $i>0$ is either empty, or for

1439: all~$x$, and~$y$ occuring in some smaller level there is a~$z$ with $x \prec z

1440: \prec y$ and $z \in i$.

1441: 

1442: To see this, consider the relevant part of the antecedent, $B = \forall

1443: i\bigl[ \forall x, y\forall j\forall k\exists z\,D \lor \forall x\neg(x \in

1444: i)\bigr]$.  If $\I(B) = 1$, then for all $i$, either \( \I(\forall x, y\forall

1445: j\forall k\exists z\,D) = 1 \) or $\I(\forall x\neg(x \in i)) = 1$. In the

1446: first case, we have \( \I(\exists z\,D) = 1 \) for all $x$, $y$, $j$, and $k$.

1447: Now suppose that for all $z$, $\I(D) < 1$, yet $\I(\exists z\, D) = 1$.  Then

1448: for at least some $z$ the value of that formula would have to be $> \I(\exists

1449: z\, P(z))$, which is impossible.  Thus, for every $x$, $y$, $j$, $k$, there is

1450: a $z$ such that $\I(D) = 1$.  But this means that for all $x$, $y$ s.t. $x \in

1451: j$, $y \in k$ with $j, k \le i$ and $x \prec y$ there is a~$z$ with $x \prec z

1452: \prec y$ and $z \in i+1$.

1453: 

1454: In the second case, where $\I(\forall x\neg(x \in i)) = 1$, we have

1455: that $\I(\neg (x \in i)) = 1$ for all $x$, hence $\I(x \in i) = 0$ and

1456: level~$i$ is empty.

1457: 

1458: Note that the non empty levels can be distributed over the whole range

1459: of the non-standard model, but since $V$ contains no dense subset, the

1460: total number of non empty levels is finite. Thus, $A$ is false in the

1461: classical interpretation $\I^c$ obtained from $\I$ by restricting $\I$

1462: to the domain $\{ i \suchthat \exists x (x\in i)\}$ and 

1463: $\I^c(Q) = \I(\neg\neg Q)$ for atomic $Q$.

1464: \end{proof}

1465: 

1466: This shows that no infinite-valued Gödel logic whose set of truth values does

1467: not contain a dense subset, i.e., no countably infinite Gödel logic is

1468: axiomatizable.  We strengthen this result in Section~\ref{sec:prenex} to show

1469: that the prenex fragments are likewise not axiomatizable.

1470: 

1471: 

1472: 

1473: % Local Variables:

1474: % TeX-master: "bpz"

1475: % End:

1476: 

1477: 

1478: \section{Uncountable Gödel sets}

1479: 

1480: \subsection{$0$ is contained in the perfect kernel\label{ssec:perfect}}

1481: 

1482: If $V$ is uncountable, and $0$ is contained in $V^\infty$, then $\gdl V$ is

1483: axiomatizable.  Indeed, Theorem~\ref{thm:gs-id} showed that the sets of

1484: validities of all such~$V$ coincide.  Thus, it is only necessary to establish

1485: completeness of the axioms system $\H$ with respect to $\gdl \bbR$. This

1486: result has been shown by several people over the years.  We give here a

1487: generalization of the proof of Takano \cite{takano}.

1488: 

1489: \begin{theorem}[Strong completeness of Gödel logic \cite{takano}]

1490:   \label{thm:takano}\hskip0pt plus 3pt minus0pt

1491:   If $\Gamma \entails A$ in $\gdl \R$, then 

1492:   $\Gamma \proves_\H A$.

1493: \end{theorem}

1494: 

1495: \begin{proof}

1496:   Assume that $\Gamma \nproves A$, we construct an interpretation~$\I$ in

1497:   which $\I(A) = 1$ for all $B \in \Gamma$ and $\I(A) < 1$. Let $y_1$, $y_2$,

1498:   \dots{} be a sequence of free variables which do not occur in $\Gamma \cup

1499:   \Delta$, let $\cT$ be the set of all terms in the language of $\Gamma \cup

1500:   \Delta$ together with the new variables~$y_1$, $y_2$, \dots, and let $\cF =

1501:   \{F_1, F_2, \ldots\}$ be an enumeration of the formulas in this language in

1502:   which $y_i$ does not appear in $F_1$, \dots, $F_i$ and in which each formula

1503:   appears infinitely often.

1504:   

1505:   If $\Delta$ is a set of formulas, we write $\Gamma \Proves \Delta$ if for

1506:   some $A_1$, \dots, $A_n \in \Gamma$, and some $B_1$, \dots, $B_m \in

1507:   \Delta$, $\proves_\H (A_1 \land \ldots \land A_n) \limp (B_1 \lor \ldots

1508:   \lor B_m)$ (and $\nProves$ if this is not the case).  We define a sequence

1509:   of sets of formulas $\Gamma_n$, $\Delta_n$ such that $\Gamma_n \nProves

1510:   \Delta_n$ by induction. First, $\Gamma_0 = \Gamma$ and $\Delta_0 = \{A\}$.

1511:   By the assumption of the theorem, $\Gamma_0 \nProves \Delta_0$.

1512:   

1513:   If $\Gamma_n \Proves \Delta_n \cup \{F_n\}$, then $\Gamma_{n+1} = \Gamma_n

1514:   \cup \{F_n\}$ and $\Delta_{n+1} = \Delta_n$.  In this case, $\Gamma_{n+1}

1515:   \nProves \Delta_{n+1}$, since otherwise we would have $\Gamma_n \Proves

1516:   \Delta_n \cup \{F_n\}$ and $\Gamma_{n} \cup \{F_n\} \Proves \Delta_n$.  But

1517:   then, we'd have 

1518:   that $\Gamma_n \Proves \Delta_n$, which contradicts the induction hypothesis

1519:   (note that $\proves_\H (A \limp B \lor F) \limp ((A \land F \limp B) \limp

1520:   (A \limp B))$).

1521:  

1522:   If $\Gamma_n \nProves \Delta_n \cup \{F_n\}$, then $\Gamma_{n+1} = \Gamma_n$

1523:   and $\Delta_{n+1} = \Delta_n \cup \{F_n, B(y_n)\}$ if $F_n \equiv \forall

1524:   x\, B(x)$, and $\Delta_{n+1} = \Delta_n \cup \{F_n\}$ otherwise.  In the

1525:   latter case, it is obvious that $\Gamma_{n+1} \nProves \Delta_{n+1}$.  In the

1526:   former, observe that by $I10$ and $\axqs$, if $\Gamma_{n} \Proves \Delta_n

1527:   \cup \{\forall x\, B(x), B(y_n)\}$ then also $\Gamma_n \Proves \Delta_n \cup

1528:   \{\forall x\, B(x)\}$ (note that $y_n$ does not occur in $\Gamma_n$ or

1529:   $\Delta_n$).

1530:   

1531:   Let $\Gamma^* = \bigcup_{i=0}^\infty \Gamma_i$ and $\Delta^* =

1532:   \bigcup_{i=0}^\infty \Delta_i$. We have:

1533:   \begin{compactenum}

1534:   \item $\Gamma^* \nProves \Delta^*$, for otherwise there would be a $k$ so

1535:     that $\Gamma_k \Proves \Delta_k$.

1536:   \item $\Gamma \subseteq \Gamma^*$ and $\Delta \subseteq \Delta^*$ (by

1537:     construction).

1538:   \item $\Gamma^* = \cF \setminus \Delta^*$, since each $F_n$ is either in

1539:     $\Gamma_{n+1}$ or $\Delta_{n+1}$, and if for some $n$, $F_n \in \Gamma^*

1540:     \cap \Delta^*$, there would be a~$k$ so that $F_n \in \Gamma_k \cap

1541:     \Delta_k$, which is impossible since $\Gamma_k \nProves \Delta_k$.

1542:   \item If $\Gamma^* \Proves B_1 \lor \ldots \lor B_n$, then~$B_i \in \Gamma^*$

1543:     for some~$i$.  For suppose not, then for $i = 1$, \dots, $n$, $B_i

1544:     \notin \Gamma^*$, and hence, by (3), $B_i \in \Delta^*$.  But then

1545:     $\Gamma^* \Proves \Delta^*$, contradicting~(1).

1546:   \item If $B(t)\in \Gamma^*$ for every~$t \in \cT$, then~$\forall x\, B(x)

1547:     \in \Gamma^*$.  Otherwise, by (3), $\forall x\, B(x) \in \Delta^*$ and so

1548:     there is some $n$ so that $\forall x\, B(x) = F_n$ and $\Delta_{n+1}$

1549:     contains $\forall x\, B(x)$ and $B(y_n)$.  But, again by (3), then $B(y_n)

1550:     \notin \Gamma^*$.

1551:   \item $\Gamma^*$ is closed under provable implication, since if $\Gamma^*

1552:     \Proves A$, then $A \notin \Delta^*$ and so, again by (3), $A \in

1553:     \Gamma^*$.  In particular, if $\proves_\H A$, then $A \in \Gamma^*$.

1554:   \end{compactenum}

1555:   

1556:   Define relations~$\lee$ and~$\equiv$ on~$\cF$ by

1557:   \[

1558:   B\lee C \dequiv B \limp C \in \Gamma^* \quad\text{and}\quad 

1559:   B\equiv C \dequiv B \lee C\land C \lee B.

1560:   \] 

1561:   Then~$\lee$ is reflexive and transitive, since for every~$B$, $\proves_\H B

1562:   \limp B$ and so $B \limp B \in \Gamma^*$, and if $B \limp C \in \Gamma^*$ and

1563:   $C\limp D \in \Gamma^*$ then $B\limp D \in \Gamma^*$, since $B \limp C, C

1564:   \limp D \Proves B \limp D$ (recall (6) above). Hence, $\equiv$ is an

1565:   equivalence relation on~$\cF$. For every~$B$ in~$\cF$ we let~$\eval{B}$ be

1566:   the equivalence class under~$\equiv$ to which~$B$ belongs, and~$\Feq$ the

1567:   set of all equivalence classes. Next we define the relation~$\le$ on~$\Feq$

1568:   by

1569:   \[

1570:   \eval{B} \le \eval{C} \dequiv B \lee C \dequiv B \limp C \in \Gamma^*.

1571:   \]

1572:   Obviously, $\le$ is independent of the choice of representatives $A$, $B$.

1573: 

1574: \begin{lemma}\label{lm:feq}

1575:   $\lF$ is a countably linearly ordered structure with

1576:   distinct maximal element~$\eval{\top}$ and minimal

1577:   element~$\eval{\bot}$.

1578: \end{lemma}

1579: 

1580: \begin{proof} 

1581:   Since~$\cF$ is countably infinite, $\Feq$ is countable. For every~$B$

1582:   and~$C$, $\proves_\H (B \limp C) \lor (C \limp B)$ by $\axlin$, and so

1583:   either~$B \limp C\in \Gamma^*$ or~$C \limp B \in \Gamma^*$ (by (4)),

1584:   hence~$\le$ is linear. For every~$B$, $\proves_\H B \limp \top$ and

1585:   $\proves_\H \bot \limp B$, and so~$B \limp \top \in \Gamma^*$ and $\bot

1586:   \limp B \in \Gamma^*$, hence~$\eval{\top}$ and~$\eval{\bot}$ are the maximal

1587:   and minimal elements, respectively. Pick any $A$ in $\Delta^*$. Since~$\top

1588:   \limp \bot \Proves A$, and~$A \notin \Gamma^*$, $\top \limp

1589:   \bot \notin \Gamma^*$, so~$\eval{\top} \neq \eval{\bot}$.

1590: \end{proof}

1591: 

1592: We abbreviate~$\eval{\top}$ by~$\one$ and~$\eval{\bot}$ by~$\zero$.

1593: 

1594: \begin{lemma}\label{lm:propertiesfeq}

1595:   The following properties hold in~$\lF$:

1596:   \begin{compactenum}

1597:   \item $\eval{B} = \one \dequiv B\in \Gamma^*$.

1598:   \item $\eval{B\land C} = \min\{\eval{B},\eval{C}\}$.

1599:   \item $\eval{B\lor C} = \max\{\eval{B},\eval{C}\}$.

1600:   \item $\eval{B\limp C} = \one$ if $\eval{B} \le \eval{C}$, $\eval{B \limp

1601:       C}=\eval{C}$ otherwise.

1602:   \item $\eval{\lnot B} = \one$ if $\eval{B} = \zero$; $\eval{\lnot B} =

1603:     \zero$ otherwise.

1604:   \item $\eval{\qe xB(x)} = \sup\{\eval{B(t)} \suchthat t\in\cT\}$.

1605:   \item $\eval{\qa xB(x)} = \inf\{\eval{B(t)} \suchthat t\in\cT\}$.

1606: 

1607:   \end{compactenum}

1608: \end{lemma}

1609: 

1610: \begin{proof} 

1611:   (1) If $\eval{B} = \one$, then $\top \impl B \in \Gamma^*$, and hence $B \in

1612:   \Gamma^*$.  And if $B \in \Gamma^*$, then $\top \limp B \in \Gamma^*$ since

1613:   $B \Proves \top \impl B$.  So $\eval{\top} \le \eval{B}$.  It follows that

1614:   $\eval{\top} = \eval{B}$ as also $\eval{B} \le \eval{\top}$.

1615:   

1616:   (2) From~$\Proves B \land C \limp B$, $\Proves B \land C \limp C$ and $D

1617:   \limp B, D \limp C \Proves D \limp B\land C$ for every~$D$, it follows that

1618:   $\eval{B \land C} = \inf \{\eval{B}, \eval{C}\}$, from which (2) follows

1619:   since~$\le$ is linear. (3) is proved analogously.

1620:   

1621:   (4) If $\eval{B} \le \eval{C}$, then $B \limp C \in \Gamma^*$, and since

1622:   $\top \in \Gamma^*$ as well, $\eval{B \limp C} = \one$.  Now suppose that

1623:   $\eval{B} \nleq \eval{C}$. From $B \land (B \limp C) \Proves C$ it follows

1624:   that $\min \{\eval{B}, \eval{B \limp C}\} \le \eval{C}$.  Because $\eval{B}

1625:   \nleq \eval{C}$, $\min \{\eval{B}, \eval{B \limp C}\} \neq \eval{B}$, hence

1626:   $\eval{B \limp C} \le \eval{C}$.  On the other hand, $\proves C \limp (B

1627:   \limp C)$, so $\eval{C} \le \eval{B \limp C}$.

1628:   

1629:   (5) If $\eval{B} = \zero$, $\lnot B = B \impl \bot \in \Gamma^*$, and hence

1630:   $\eval{\lnot B} = \one$ by (1).  Otherwise, $\eval{B} \nleq \eval{\bot}$,

1631:   and so by (4), $\eval{\lnot B} = \eval{B \limp \bot} = \zero$.

1632:   

1633:   (6) Since $\proves_\H B(t)\limp \qe x\, B(x)$, $\eval{B(t)} \le \eval{\qe

1634:     x\, B(x)}$ for every~$t\in\cT$. On the other hand, for every~$D$ without

1635:   $x$ free,

1636:   \begin{align*}

1637:     &&&\eval{B(t)} \le \eval{D} && \qquad\mbox{for every $t\in\cT$}\\

1638:     &\dequiv&& B(t)\limp D\in \Gamma^*&&\qquad\mbox{for every $t\in\cT$}\\

1639:     &\Rightarrow&& \qa x(B(x)\limp D)\in\Gamma^* &

1640:               & \qquad\text{by property (5) of $\Gamma^*$}\\

1641:     &\Rightarrow&& \qe x\,B(x) \limp D \in\Gamma^* &&\qquad

1642:     \mbox{since $\qa x(B(x)\limp D) \Proves \qe x\,B(x)\limp D$}\\

1643:     &\dequiv&& \eval{\qe x\, B(x)}\le \eval{D}.

1644:   \end{align*}

1645:   (7) is proved analogously.

1646: \end{proof}

1647: 

1648: $\lF$ is countable, let $\zero = a_0, \one = a_1, a_2, \ldots$ be an

1649: enumeration. Define $h(\zero) = 0$, $h(\one) = 1$, and define~$h(a_n)$

1650: inductively for $n>1$: Let

1651: $ a_n^- = \max\{a_i\suchthat i<n \text{ and } a_i < a_n\}$ and

1652: $ a_n^+ = \min\{a_i\suchthat i<n \text{ and } a_i > a_n\}$, and define 

1653: $h(a_n) = (h(a_n^-) + h(a_n^+))/2$ (thus, $a_2^-=\zero$ and

1654: $a_2^+=\one$ as $\zero=a_0<a_2<a_1=\one$, hence $h(a_2)=\frac12$).

1655: Then $h\colon \lF \to \bbQ \cap [0,1]$ is a strictly monotone map

1656: which preserves infs and sups.  By

1657: Lemma~\ref{lemma:countable-into-cantor} there exists a

1658: \g-embedding~$h'$ from~$\bbQ \cap [0, 1]$ into~$\lR$ which is also

1659: strictly monotone and preserves infs and sups. Put~$\I(B) =

1660: h'(h(\eval{B}))$ for every atomic~$B\in\cF$ and we obtain a

1661: $V_\R$-interpretation.

1662: 

1663: Note that for every~$B$, $\I(B) = 1$ iff $\eval{B} = \one$ iff $B \in

1664: \Gamma^*$. Hence, we have $\I(B) = 1$ for all $B \in \Gamma$ while if $A

1665: \notin \Gamma^*$, then~$\I(A) < 1$, so~$\Gamma \nentails A$.  Thus we have

1666: proven that on the assumption that if $\Gamma \nproves A$, then $\Gamma

1667: \nentails A$

1668: \end{proof}

1669: 

1670: As already mentioned we obtain from this completeness proof together with the

1671: soundness theorem (Theorem~\ref{thm:soundness}) and Theorem~\ref{thm:gs-id}

1672: the characterization of recursive axiomatizability:

1673: 

1674: \begin{theorem}\label{thm:fo:zeroinP}

1675:   Let $V$ be a Gödel set with $0$ contained in the perfect kernel of $V$.

1676:   Suppose that $\Gamma$ is a set of closed formulas. Then $\Gamma \entails_V

1677:   A$ iff $\Gamma \proves_\H A$.

1678: \end{theorem}

1679: 

1680: \begin{corollary}[Deduction theorem for Gödel logics]\label{thm:deduction}

1681:   Suppose that $\Gamma$ is a set of formulas, and $A$ is a closed formula.

1682:   Then

1683:   \[

1684:   \Gamma, A \proves_\H B \quad \text{iff} \quad \Gamma \proves_\H  A \limp B.

1685:   \]

1686: \end{corollary}

1687: 

1688: \begin{proof} 

1689:   Use the soundness theorem (Theorem~\ref{thm:soundness}), completeness

1690:   theorem (Theorem~\ref{thm:fo:zeroinP}) and the semantic deduction

1691:   theorem~\ref{thm:semdeduc}.  Another proof would be by induction on the

1692:   length of the proof. See \cite{hajek}, Theorem~2.2.18.

1693: \end{proof}

1694: 

1695: \subsection{$0$ is isolated\label{ssec:isolated}}

1696: 

1697: In the case where $0$ is isolated, and thus also not contained in the

1698: perfect kernel, we will transform a counter example in $\GR$ for

1699: $\Gamma,\Pi\entails A$, where $\Pi$ is a set of sentences stating that 

1700: every infimum is a minimum, into a counter example in $\gdl V$ 

1701: for $\Gamma\entails A$.

1702: 

1703: \begin{lemma}\label{lm:equivaxioms}

1704:   Let $x,\bar y$ be the free variables in $A$.

1705:   \[ 

1706:      \proves_{\Ho} \forall\bar y(\lnot \forall x\, A(x,\bar y) \limp

1707:      \exists x\, \lnot A(x,\bar y))

1708:    \]

1709: \end{lemma}

1710: 

1711: \begin{proof}

1712:   It is easy to see that in all Gödel logics the following weak form of the

1713:   law of excluded middle is valid: $\lnot\lnot A(a) \lor \lnot A(a)$.  By

1714:   quantification we obtain $\qa x \lnot\lnot A(x) \lor \qe x \lnot A(x)$ and

1715:   by valid quantifier shifting rules $\lnot\lnot \qa x\, A(x) \lor \qe \lnot

1716:   A(x)$.  From the intuitionistically valid $\lnot A\lor B \limp (A \limp B)$

1717:   we can prove $\lnot \qa x\, A(x) \limp \qe x \lnot A(x)$. A final

1718:   quantification of the free variables concludes the proof.

1719: \end{proof}

1720: 

1721: \begin{theorem}\label{thm:fo:iso}

1722:   Let $V$ be an uncountable Gödel set where $0$ is isolated.  Suppose $\Gamma$

1723:   is a set of closed formulas.  Then $\Gamma \entails_V A$ iff $\Gamma

1724:   \proves_{\Ho} A$.

1725: \end{theorem}

1726: 

1727: \begin{proof}

1728:   If: Follows from soundness (Theorem~\ref{thm:soundness}) and the observation

1729:   that $\axiso$ is valid for any $V$ where $0$ is isolated.

1730:   

1731:   Only if: We already know from Theorem~\ref{thm:gs-id} that the entailment

1732:   relation of $V$ and $V \cup [\inf P,1]$ coincide, where $P$ is the perfect

1733:   kernel of $V$. So we may assume wthout loss of generality that $V$ already

1734:   is of this form, i.e.\ that $\lambda = \inf P$ and $V \cap [\lambda, 1] =

1735:   [\lambda, 1]$. Let $V' = [0,1]$.  Define

1736:   \[

1737:   \Pi = \{\qa{\bar y}(\lnot\qa x\, A(x,\bar y) \limp \qe x\lnot A(x,\bar y))

1738:   \suchthat A(x,\bar y) \mbox{ formula}\}

1739:   \] 

1740:   where $A(x,\bar y)$ ranges over \emph{all} formulas with free variables $x$

1741:   and $\bar y$. We consider the entailment relation in $V'$. Either $\Pi,

1742:   \Gamma \entails_{V'} A$ or $\Pi, \Gamma \nentails_{V'} A$.  In the former

1743:   case we know from the strong completeness of $\H$ for $\GR$ that there are

1744:   finite subsets $\Pi'$ and $\Gamma'$ of $\Pi$ and $\Gamma$, respectively,

1745:   such that $\Pi', \Gamma' \proves_{\H} A$.  Since all the sentences in $\Pi$

1746:   are provable in $\Ho$ (see Lemma~\ref{lm:equivaxioms}) we obtain that

1747:   $\Gamma' \proves_{\Ho} A$.  In the latter case there is an interpretation

1748:   $\I'$ such that

1749:   \[

1750:    \inf \{ \I'(G) \suchthat G\in \Pi \cup \Gamma \} > \I'(A).

1751:   \]

1752:   It is obvious from the structure of the formulas in $\Pi$ that their truth

1753:   value will always be either $0$ or $1$. Combined with the above we know that

1754:   for all $G \in \Pi$, $\I'(G) = 1$.  Next we define a function $f(x)$ which

1755:   maps values from $\subval(\I', \Gamma \cup \Pi \cup\{A\})$ into $V$:

1756:   \[

1757:      f(x) = \begin{cases} 0 & x=0\\

1758:                           \lambda + x/(1-\lambda) & x>0 

1759:              \end{cases}

1760:   \]

1761:   We see that $f$ satisfies conditions~(1) and~(2) of

1762:   Lemma~\ref{lem:induced-interpretation}, but we cannot use

1763:   Lemma~\ref{lem:induced-interpretation} directly, as not all existing infima

1764:   and suprema are necessarily preserved.

1765:   

1766:   Consider as in Lemma~\ref{lem:induced-interpretation} the interpretation

1767:   $\I_f(B) = f(\I'(B))$ for atomic subformulas of $\Gamma \cup \Pi \cup\{A\}$.

1768:   We want to show that the identity $\I_f(B) = f(\I'(B))$ extends to all

1769:   subformulas of $\Gamma\cup \Pi \cup \{A\}$. For propositional connectives

1770:   and the existentially quantified formulas this is obvious.  The important

1771:   case is $\qa x\, A(x)$. First assume that $\I'(\qa x\, A(x)) > 0$. Then it

1772:   is obvious that $\I_f(\qa x\, A(x)) = f(\I'(\qa x\, A(x)))$. In the case

1773:   where $\I'(\qa x\, A(x)) = 0$ we observe that $A(x)$ contains a free

1774:   variable and therefore $\lnot \qa x\, A(x) \limp \qe x \lnot A(x) \in \Pi$,

1775:   thus $\I'(\lnot \qa x\, A(x) \limp \qe x\lnot A(x)) = 1$. This implies that

1776:   there is a witness $c$ such that $\I'(A(c)) = 0$. Using the induction

1777:   hypothesis we know that $\I_f(A(c)) = 0$, too. We obtain that $\I_f(\qa x\,

1778:   A(x)) = 0$, concluding the proof.

1779:   

1780:   Thus we have shown that $\I_f$ is a counterexample to $\Gamma \entails_V A$

1781:   which completes the proof of the theorem.

1782: \end{proof}

1783: 

1784: \subsection{$0$ not isolated but not in the perfect kernel}\label{sec:uncount-nonax}

1785: 

1786: In the preceding sections, we gave axiomatizations for the logics based on

1787: those uncountably infinite Gödel sets~$V$ where $0$ is either isolated or in

1788: the perfect kernel of~$V$.  It remains to determine whether logics based on

1789: uncountable Gödel sets where $0$ is neither isolated nor in the perfect kernel

1790: are axiomatizable.  The answer in this case is negative.  If $0$ is not

1791: isolated in $V$, $0$ has a countably infinite neighborhood.  Furthermore, any

1792: sequence $(a_n)_{n \in \N} \to 0$ is so that, for sufficiently large $n$, $V

1793: \cap [0, a_n]$ is countable and hence, by (the proof of)

1794: Theorem~\ref{bendixon}, contains no densely ordered subset.  This fact is the

1795: basis for the following non-axiomatizability proof, which is a variation on

1796: the proof of Theorem~\ref{thm:count-nonax}.

1797: 

1798: \begin{theorem}\label{thm:uncount-noniso-nonax}

1799:   If $V$ is uncountable, $0$ is not isolated in $V$, but not in the perfect

1800:   kernel of~$V$, then $\gdl{V}$ is not axiomatizable.

1801: \end{theorem}

1802: 

1803: \begin{proof}

1804:   We show that for every sentence $A$ there is a sentence $A^h$ s.t. $A^h$ is

1805:   valid in $\gdl V$ iff $A$ is true in every finite (classical) first-order

1806:   structure.

1807:   

1808:   The definition of $A^h$ mirrors the definition of $A^g$ in the proof of

1809:   Theorem~\ref{thm:count-nonax}, except that the construction there is carried

1810:   out infinitely many times for $V \cap [0, a_n]$, where $(a_n)_{n \in \N}$ is

1811:   a strictly descending sequence, $a_n > 0$ for all $n$, which converges

1812:   to~$0$.  Let $P$ be a binary and $L$ be a ternary predicate symbol not

1813:   occurring in~$A$ and let $R_1$, \dots, $R_n$ be all the predicate symbols

1814:   in~$A$.  We use the abbreviations $x \in_\ell y \equiv \neg\neg L(x, y,

1815:   \ell)$ and $x \prec_\ell y \equiv (P(y, \ell) \impl P(x, \ell)) \impl P(y,

1816:   \ell)$.  As before, for a fixed $\ell$, provided $\I(\exists x\, P(x, \ell))

1817:   < 1$, $\I(x \prec_\ell y) = 1$ iff $\I(P(x, \ell)) < \I(P(y, \ell))$, and

1818:   $\I(x \in_\ell y)$ is always either $0$ or $1$.  We also need a binary

1819:   predicate symbol $Q(\ell)$ to give us the descending

1820:   sequence~$(a_n)_{n\in\N}$: Note that $\I(\neg \forall \ell\, Q(\ell)) = 1$

1821:   iff $\inf \{\I(Q(d)) : d \in \card{\I}\} = 0$ and $\I(\exists \ell\, \neg

1822:   Q(\ell)) = 1$ iff $0 \notin \{\I(Q(d)) : d \in \card{\I}\}$.

1823:   

1824:   Let $A^h \equiv$

1825:   \begin{equation}\label{fm:0notiso}

1826:     \left\{

1827:       \begin{array}{l}

1828:         S \land  

1829:         \forall \ell((Q(s(\ell)) \impl Q(\ell)) \impl Q(s(\ell)) \land {}\\

1830:         \quad \neg \forall \ell\, Q(\ell) \land \exists \ell\, \neg Q(\ell) \land {}\\

1831:         \quad \forall \ell\forall x((Q(\ell) \impl P(x, \ell)) \impl Q(\ell)) \land {}\\ 

1832:         \quad \forall \ell \exists x\exists y(x \in_\ell 0 \land {} y \in_\ell 0 \land 

1833:         x \prec_\ell y) \land {}\\

1834:         \quad 

1835:         \quad \forall \ell\forall i\bigl[\forall x, y \forall j \forall k \exists z\, E

1836:         \lor \forall x\neg(x \in_\ell s(i))\bigr]

1837:       \end{array}

1838:     \right\}

1839:     \impl (A' \lor \exists \ell \exists u\, P(u, \ell) \lor \exists \ell\, Q(\ell))

1840:   \end{equation}

1841:   where $S$ is the conjunction of the standard axioms for $0$, successor and

1842:   $\le$, with double negations in front of atomic formulas,

1843:   \[ 

1844:   E\equiv \begin{array}{l}

1845:     (j \le i \land x \in_\ell j \land k\le i \land y \in_\ell k \land x \prec_\ell y) \impl {}\\

1846:     \qquad \impl (z \in_\ell s(i) \land x \prec_\ell z \land z \prec_\ell y)

1847:   \end{array}

1848:   \]

1849:   and $A'$ is $A$ where every atomic formula is replaced by its double

1850:   negation, and all quantifiers are relativized to the predicate

1851:   $R(\ell)\equiv \forall i\exists x(x \in_\ell i)$.

1852:   

1853:   The idea here is that an interpretation $\I$ will define a sequence

1854:   $(a_n)_{n\in\N} \to 0$ by $a_n = \I(Q(\bar{n}))$ where $a_n > a_{n+1}$, and

1855:   $0 < a_n < 1$ for all~$n$.  Let $L_\ell^i = \{x : \I(x \in_\ell i)\}$ be the

1856:   $i$-th $\ell$-level.  $P(x, \ell)$ orders the set $\bigcup_i L_\ell^i = \{x

1857:   : \I(\exists i\, x \in_\ell i) = 1\}$ in a subordering of $V \cap [0, a_n]$:

1858:   $x \prec_\ell y$ iff $\I(x \prec_\ell y) = 1$.  Again we force that whenever

1859:   $x, y \in L_\ell^i$ with $x \prec_\ell y$, there is a $z \in L_\ell^{i+1}$

1860:   with $x \prec_\ell z \prec_\ell y$, or, if no possible such $z$ exists,

1861:   $L_\ell^{i+1} = \emptyset$.  Let $r(\ell)$ be the least $i$ so that

1862:   $L_\ell^i$ is empty, or $\infty$ otherwise.  If $r(\ell) = \infty$ then

1863:   there is a densely ordered subset of $V \cap [0, a_\ell]$.  So if $0$ is not

1864:   in the perfect kernel, for some sufficiently large $L$, $r(\ell) < \infty$

1865:   for all $\ell > L$.  $\I(R(\ell)) = 1$ iff $r(\ell) = \infty$ hence $\{\ell

1866:   : \I(R(\ell)) = 1\}$ is finite whenever the interpretations of $P$, $L$, and

1867:   $Q$ are as intended.

1868:   

1869:   Now if $A$ is classically false in some finite structure~\I, we can again

1870:   choose a $\gdl{V}$-interpretation $\I^h$ in which the interpretations of

1871:   $P$, $Q$, $L$ are as intended, the number theoretic predicates and functions

1872:   receive their standard interpretation, there are as many $\ell$ with

1873:   $\I^h(R(\ell)) = 1$ as there are elements in the domain of $\I$, and the

1874:   predicates of $A$ behave on $\{\ell : \I(R(\ell)) = 1\}$ just as they do

1875:   on~$\I$.  $\I^h \nmodels A^h$.

1876:   

1877:   On the other hand, if $\I \nmodels A^h$, then the value of the consequent is

1878:   $< 1$.  Then as required, for all $x$, $\ell$, $\I(P(x, \ell)) < 1$ and

1879:   $\I(Q(\ell)) < 1$.  Since the antecedent, as before, must be $=1$, this

1880:   means that $x \prec_\ell y$ expresses a strict ordering of the elements of

1881:   $L_\ell^i$ and $\I(((Q(s(\ell) \impl Q(\ell)) \impl Q(s(\ell))) = 1$ for all

1882:   $\ell$ guarantees that $\I(Q(s(\ell))) = a_{n+1} < a_n = \I(Q(\ell))$.  The

1883:   other conditions are likewise seen to hold as intended, so that we can

1884:   extract a finite countermodel for $A$ based on the interpretation of the

1885:   predicate symbols of $A$ on $\{\ell : \I(R(\ell)) = 1\}$, which must be

1886:   finite.

1887: \end{proof}

1888: 

1889: 

1890: 

1891: \section{Fragments}\label{sec:fragments}

1892: 

1893: \fxnote{Für welche Fragmente kann/soll man starke vollständigkeit (im

1894:   axiomatisierbaren Fall) zeigen?}

1895: 

1896: \subsection{Prenex fragments}\label{sec:prenex}

1897: 

1898: One interesting restriction of the axiomatizability problem is the question

1899: whether the prenex fragment of $\gdl{V}$, i.e., the set of prenex formulas

1900: valid in $\gdl{V}$, is axiomatizable.  This is non-trivial, since in general

1901: in Gödel logics, arbitrary formulas are not equivalent to prenex formulas.

1902: Thus, so far the proofs of non-axiomatizability of the logics treated in

1903: Sections~\ref{sec:countable} and~\ref{sec:uncount-nonax} do not establish the

1904: non-axiomatizability of their prenex fragments, nor do they exclude the

1905: possibility that the corresponding prenex fragments are r.e.  We investigate

1906: this question in this section, and show that the prenex fragments of all

1907: finite and uncountable Gödel logics are r.e., and that the prenex fragments of

1908: all countably infinite Gödel logics are not r.e.  The axiomatizability result

1909: is obtained from a version of Herbrand's Theorem for finite and

1910: uncountably-valued Gödel logics, which is of independent interest.  The

1911: non-axiomatizability of countably infinite Gödel logics is obtained as a

1912: corrolary of Theorem~\ref{thm:count-nonax}.

1913: 

1914: Let $V$ be a Gödel set which is either finite or uncountable. Let $\Gd$ be a

1915: Gödel logic with such a truth value set. We show how to effectively associate

1916: with each prenex formula $A$ a quantifier-free formula $A^\ast$ which is valid

1917: in $\Gd$ if and only if $A$ is a tautology.  The axiomatizability of the

1918: prenex fragment of $\Gd$ then follows from the axiomatizability of \LC{} (in

1919: the infinite-valued case) and propositional $\gdl m$ (in the finite-valued

1920: case).

1921: 

1922: \begin{definition}[Herbrand form]

1923: Given a prenex formula $A \equiv \Q_1

1924: x_1\ldots\Q_n x_n\,B(\bar x)$ ($B$ quantifier free), the

1925: \emph{Herbrand form}~$A^H$ of $A$ is $\exists x_{i_1}\ldots

1926: \exists x_{i_m}\, B(t_1, \ldots, t_n)$, where $\{x_{i_j} : 1 \le j \le

1927: m\}$ is the set of existentially quantified variables in $A$, and

1928: $t_i$ is $x_{i_j}$ if $i = i_j$, or is $f_i(x_{i_1}, \ldots, x_{i_k})$

1929: if $x_i$ is universally quantified and $k = \max \{j : i_j < i\}$. We

1930: will write $B(t_1,\ldots,t_n)$ as $B^F(x_{i_1}, \ldots, x_{i_m})$ if

1931: we want to emphasize the free variables.

1932: \end{definition}

1933: 

1934: \begin{lemma}

1935: \label{skolemization}

1936: If $A$ is prenex and $\modelsg A$, then $\modelsg A^H.$

1937: \end{lemma}

1938:  

1939: \begin{proof}

1940: Follows from the usual laws of quantification, which are valid in all Gödel

1941: logics.

1942: \end{proof}

1943: 

1944: Our next main result will be Herbrand's theorem for $\gdl V$ for $V$

1945: uncountable or finite.  The {\em Herbrand universe} $\HU(B^F)$ of

1946: $B^F$ is the set of all variable-free terms which can be constructed

1947: from the set of function symbols occurring in $B^F$. To prevent

1948: $\HU(B^F)$ from being finite or empty we add a constant and a function

1949: symbol of positive arity if no such symbols appear in~$B^F$.  The {\em

1950:   Herbrand base} $\HB(B^F)$ is the set of atoms constructed from the

1951: predicate symbols in $B^F$ and the terms of the Herbrand universe. In

1952: the next theorem we will consider the Herbrand universe of a formula

1953: $\exists \tup{x}\, B^F(\tup{x})$.  We fix a non-repetitive enumeration

1954: $C_1$, $C_2$, \dots of $\HB(B^F)$, and let 

1955: $X_\ell = \{\bot, C_1, \ldots, C_\ell, \top\}$ (we may take $\top$ to

1956: be a formula which is always $=1$). $B^F(\tup{t})$ is an

1957: \emph{$\ell$-instance} of $B^F(\tup{x})$ if the atomic subformulas of

1958: $B^F(\tup{t})$ are in $X_\ell$. 

1959: 

1960: \begin{definition} 

1961:   An $\ell$-\emph{constraint} is a non-strict linear ordering

1962:   $\preceq$ of $X_\ell$ s.t. $\bot$ is minimal and $\top$ is maximal.

1963:   An interpretation~$\I$ {\em fulfils} the constraint $\preceq$

1964:   provided for all $C, C' \in X_\ell$, $C \preceq C'$ iff 

1965:   $\I(C) \le \I(C')$.  We say that the constraint $\preceq'$ on

1966:   $X_{\ell+1}$ \emph{extends} $\preceq$ if for all $C, C' \in X_\ell$,

1967:   $C \preceq C'$ iff $C \preceq' C'$.

1968: \end{definition}

1969: 

1970: Lemma~\ref{lem:g-embed} showed that if $h: V \to W$ is a \g-embedding and $\I$

1971: is a $V$-interpretation, then $h(\I(A)) = \I_h(A)$ for any formula~$A$.  If no

1972: quantifiers are involved in $A$, this also holds without the requirement of

1973: continuity.  For the following proof we need a similar notion.  Let $V$ be a

1974: Gödel sets, $X$ a set of atomic formulas, and suppose there is an

1975: order-preserving, strictly monotone $h\colon \{\I(C)\colon C \in X\} \to V$

1976: which is so that $h(1) = 1$ and $h(0) = 0$.  Call any such $h$ a \emph{truth

1977: value injection on $X$}.  Now suppose $B$ is a quantifier-free formula, and

1978: $X$ its set of atomic subformulas.  Two interpretations $\I$, $\J$ are

1979: \emph{compatible on $X$} if $\I(C) \le \I(C')$ iff $\J(C) \le \J(C')$ for all

1980: $C \in X$.

1981: 

1982: \begin{proposition}\label{tviso}

1983:  Let $B^F$ be a quantifier free formula, and $X$ its set of atomic subformulas

1984:  together with $\top$, $\bot$.  If $\I$, $\J$ are compatible on $X$, then

1985:  there is a truth value injection~$h$ on $X$ with $h(\I(C^F)) = \J(C^F)$.

1986: \end{proposition}

1987: 

1988: \begin{proof}

1989: Let $h(\I(C)) = \J(C)$ for $B \in X$.  Since $\I$, $\J$ are compatible on $X$,

1990: $\I(C) \le \I(C')$ iff $\J(C) \le \J(C')$, and hence $\I(C) \le \I(C')$ iff

1991: $h(\I(C)) \le h(\J(C'))$ and $h$ is strictly monotonic.  The conditions $h(0)

1992: = 0$ and $h(1) = 1$ are satisfied by definition, since $\top$, $\bot \in X$.

1993: We get $h(\I(B^F)) = \J(B^F)$ by induction on the complexity of~$A$.

1994: \end{proof}

1995: 

1996: \begin{proposition}\label{ellI}

1997: (a) If $\preceq'$ extends $\preceq$, then every $\I$ which fulfills $\preceq'$

1998: also fulfills $\preceq$. (b) If $\I$, $\J$ fulfill the $\ell$-constraint

1999: $\preceq$, then there is a truth value injection~$h$ on $X_\ell$ with

2000: $h(\I(B^F(\tup{t}))) = \J(B^F(\tup{t}))$ for all $\ell$-instances

2001: $B^F(\tup{t})$ of $B^F(\tup{x})$; in particular, $\I(B^F(\tup{t})) = 1$ iff

2002: $\J(B^F(\tup{t})) = 1$.

2003: \end{proposition}

2004: 

2005: \begin{proof}

2006: (a) Obvious. (b) Follows from Proposition~\ref{tviso} together with the

2007:   observation that $\I$ and $\J$ both fulfill $\preceq$ iff they are

2008:   compatible on $X_\ell$.

2009: \end{proof} 

2010: 

2011: \begin{lemma} \label{univH}

2012: Let $B^F$ be a quantifier-free formula, and let $V$ be a finite or uncountably

2013: infinite Gödel set. If $\modelsg \exists \tup{x}\, B^F(\tup{x})$ then there are

2014: tuples $\tup{t}_1, \dots \overline{t}_n$ of terms in $U(B^F)$, such that

2015: $\modelsg \bigvee_{i=1}^{n} B^F(\tup{t}_i)$.

2016: \end{lemma}

2017: 

2018: \begin{proof}

2019: Suppose first that $V$ is uncountable.  By Theorem~\ref{bendixon}, $V$

2020: contains a dense linear subordering. We construct a ``semantic tree'' $\T$;

2021: i.e., a systematic representation of all possible order types of

2022: interpretations of the atoms $C_i$ in the Herbrand base.  $\T$ is a rooted

2023: tree whose nodes appear at levels.  Each node at level~$\ell$ is labelled with

2024: an $\ell$-constraint.

2025: 

2026: $\T$ is constructed in levels as follows: At level~$0$, the root of~$\T$ is

2027: labelled with the constraint $\bot < \top$.  Let $\nu$ be a node added at

2028: level $\ell$ with label $\preceq$, and let $T_\ell$ be the set of terms

2029: occurring in $X_\ell$.  Let (*) be: For every interpretation~$\I$ which

2030: fulfils~$\preceq$, there is some $\ell$-instance $B^F(\tup{t})$ so that

2031: $\I(B^F(\tup{t}))=1$. If (*) obtains, $\nu$ is a leaf node of~$\T$, and no

2032: successor nodes are added at level $\ell +1$.

2033:   

2034: Note that by Proposition~\ref{ellI}(b), any two

2035: interpretations which fulfill $\preceq$ make the same $\ell$-instances

2036: of $B^F(\tup{t})$ true; hence $\nu$ is a leaf node if and only if there

2037: is an $\ell$-instance $A(\tup{t})$ s.t. $\I(A(\tup{t})) = 1$ for

2038: all interpretations $\I$ that fulfil~$\preceq$.

2039: 

2040: If (*) does not obtain, for each $(\ell + 1)$-constraint $\preceq'$

2041: extending $\preceq$ we add a successor node $\nu'$ labelled with

2042: $\preceq'$ to $\nu$ at level $\ell+1$.

2043: 

2044: We now have two cases:

2045: 

2046: (1) $\T$ is finite. Let $\nu_1, \ldots, \nu_m$ be the leaf nodes of~$\T$ of

2047:     levels $\ell_1$, \ldots, $\ell_m$, each labelled with a constraint

2048:     $\preceq_1$, \dots, $\preceq_m$.  By (*), for each $j$ there is an

2049:     $\ell_j$-instance $B^F(\tup{t}_j)$ with $\I(B^F(\tup{t})) = 1$ for all

2050:     $\I$ which fulfill~$\preceq_j$.  It is easy to see that every

2051:     interpretation fulfills at least one of the $\preceq_j$.  Hence, for all

2052:     $\I$, $\I(B^F(\tup{t}_1) \lor \ldots \lor B^F(\tup{t}_m)) = 1$, and so

2053:     $\modelsg \bigvee_{i=1}^m B^F(\tup{t}_i)$.

2054: 

2055: (2) $\T$ is infinite.  By König's lemma, $\T$ has an infinite branch

2056:     with nodes $\nu_0$, $\nu_1$, $\nu_2$, \dots where $\nu_\ell$ is

2057:     labelled by $\preceq_\ell$ and is of level $\ell$.  Each

2058:     $\preceq_{\ell+1}$ extends $\preceq_\ell$, hence we can form

2059:     $\mathnormal{\preceq} = \bigcup_\ell \mathnormal{\preceq_\ell}$.  

2060:     Let $V' \subseteq V$ be a

2061:     non-trivial densely ordered subset of $V$, let $V' \ni c < 1$, and

2062:     let $V'' = V' \cap [0, c)$.  $V''$ is clearly also densely

2063:     ordered. Now let $V_c$ be $V'' \cup \{0, 1\}$, and let $h: B(A(x))

2064:     \cup \{\bot, \top\} \to V_c$ be an injection which is so that, for

2065:     all $A_i, A_j \in B(A(x))$, $h(A_i) \le h(A_j)$ iff $A_i \preceq

2066:     A_j$, $h(\bot) = 0$ and $h(\top) = 1$. We define an interpretation

2067:     $\I$ by: $f^{\I}(t_1, \ldots, t_n) =

2068:     f(t_1, \ldots, t_n)$ for all $n$-ary function symbols~$f$ and

2069:     $P^{\I}(t_1, \ldots, t_n) = h(P(t_1, \ldots, t_n))$ for all $n$-ary

2070:     predicate symbols~$P$ (clearly then, $\I(A_i) = h(A_i)$). By

2071:     definition, $\I$ $\ell$-fulfills $\preceq_\ell$ for all $\ell$. By

2072:     (*), $\I(A(\tup{t})) < 1$ for all $\ell$-instances $A(\tup{t})$ of

2073:     $A(x)$, and by the definition of $V_c$, $\I(A(\tup{t})) < c$.

2074:     Since every $A(\tup{t})$ with $\tup{t} \in U(A(x))$ is an

2075:     $\ell$-instance of $A(x)$ for some $\ell$, we have $\I(\exists x\,

2076:     A(\tup{x})) \le c < 1$.This contradicts the assumption that

2077:     $\modelsg \exists \tup{x}\, A(\tup{x})$.

2078: 

2079: If $V$ is finite, the proof is the similar, except simpler.  Suppose

2080: $\card{V} = n$.  Call a constraint $\preceq$

2081: \emph{$n$-admissible} if there is some $V$-interpretation $\I$ which

2082: fulfills it.  Such $\preceq$ have no more than $n$ equivalence classes under

2083: the equivalence relation $C \sim C'$ iff $C \preceq C'$ and $C' \preceq C$.

2084: In the construction of the semantic tree above, replace each mention of

2085: $\ell$-constraints by $n$-admissible $\ell$-constraints.  The argument in the

2086: case where the resulting tree is finite is the same.  If $\T$ is infinite,

2087: then the resulting order ${\preceq} = \bigcup_\ell {\preceq_\ell}$ is

2088: $n$-admissible, since all $\preceq_\ell$ are. Let $c = \max \{ b: b \in V, b <

2089: 1\}$ and $V_c = V$.  The rest of the argument goes through without change.

2090: \end{proof}

2091: 

2092: \begin{lemma}\label{lem:reskolem}

2093: Let $\exists \tup{x}\,

2094: B^F(\tup{x})$ be the Herbrand form of the prenex formula $A \equiv \tup{\Q}_i

2095: B(\tup{y}_i)$, and let $\tup{t}_1, \ldots, \tup{t}_m$ be tuples of terms in

2096: $\HU(B^F)$. If $\gdl{V} \models \bigvee_{i=1}^{m} B^F(\tup{t_i})$, then

2097: $\gdl{V} \models A.$

2098: \end{lemma}

2099: 

2100: \begin{proof} For any Gödel set $V$, the following rules are valid

2101:   in~$\gdl{V}$:

2102: 

2103: (1) $A \lor B  \vdash B \lor A$.

2104: 

2105: (2) $(A \lor B) \lor C \vdash A \lor (B \lor C)$ .

2106: 

2107: (3) $A \lor (B \lor B) \vdash A \lor B$ .

2108: 

2109: (4) $A(y) \vdash \forall x\, A(x)$.

2110: 

2111: (5) $A(t) \vdash \exists x\,  A(x)$.

2112: 

2113: (6) $\forall x (A(x) \lor B) \vdash \forall x\, A(x) \lor B$.

2114: 

2115: (7) $\exists x (A(x) \lor B) \vdash \exists x\, A(x) \lor B$.

2116: 

2117: \noindent ($x$ is not free in $B$.)  The result follows from

2118: \cite{BCF01LPAR}, Lemma~6, and are also easily verified directly.

2119: \end{proof}

2120: 

2121: \begin{theorem} \label{HT}

2122: Let $A$ be prenex, $\exists \tup{x}\, B^F(\tup{x})$ its Herbrand form, and let

2123: $V$ be a finite or uncountably infinite Gödel set. Then $\modelsg A$ iff there

2124: are tuples $\tup{t}_1, \ldots \tup{t}_m$ of terms in $\HU(B^F)$, such that

2125: $\modelsg \bigvee_{i=1}^{m} B^F(\tup{t}_i)$.

2126: \end{theorem}

2127: 

2128: \begin{proof}

2129: If: This is Lemma~\ref{lem:reskolem}.  Only if: By Lemma~\ref{skolemization}

2130: and Lemma~\ref{univH}.

2131: \end{proof}

2132: 

2133: \begin{remark} 

2134: An alternative proof of Herbrand's theorem can be obtained using the

2135: analytic calculus {\it HIF} (``Hypersequent calculus for

2136: Intuitionistic Fuzzy logic'') \cite{BaazZach00CSL}.

2137: \end{remark}

2138: 

2139: \begin{theorem}

2140: The prenex fragment of a Gödel logic based on a truth value set~$V$ which is

2141: either finite or uncountable infinite is axiomatizable. An axiomatization is

2142: given by the standard axioms and rules for~$\LC$ extended by the rules

2143: (4)--(7) of the proof of Lemma~\ref{lem:reskolem}. For the

2144: $m$-valued case add the characteristic axiom for $\gdl m$, \( G_m \equiv

2145: \bigvee_{i=1}^m\bigvee_{j=i+1}^{m+1} ((A_i \impl A_j) \land (A_j \impl A_i)).

2146: \)

2147: \end{theorem}

2148: 

2149: \begin{proof}  

2150: Completeness: Let $\tup{\Q} \tup{y}_i B(\tup{y})$ be a prenex formula valid in

2151: $\gdl V$. By Theorem~\ref{HT}, a Herbrand disjunction $\bigvee_{i=1}^{n}

2152: B^F(\tup{t}_i)$ is a tautology in $\gdl{V}$.  Hence, it is provable in \LC{}

2153: or $\LC + G_m$ \cite[Chapter 10.1]{gottwald}.  $\tup{\Q} \tup{y} B(\tup{y})$

2154: is provable by Lemma~\ref{lem:reskolem}.

2155: 

2156: Soundness: The rules in the proof of Lemma~\ref{lem:reskolem} are valid in

2157: $\gdl{V}$. In particular, note that $\forall x(A(x) \lor B) \to (\forall x\,

2158: A(x) \lor B)$ with $x$ not free in $B$ is valid in all Gödel logics, and

2159: $\exists x(A(x) \lor B) \to \exists x\, A(x) \lor B$ is already

2160: intuitionistically valid.

2161: \end{proof}

2162: 

2163: In Theorem~\ref{thm:count-nonax}, we showed that for every first-order formula

2164: $A$, there is a formula $A^g$ which is valid in $\gdl{V}$ for $V$ countably

2165: infinite iff $A$ is valid in every finite classical interpretation.  We now

2166: strengthen this result to show that the prenex fragment of $\gdl{V}$ (for $V$

2167: countably infinite) is likewise not axiomatizable.  This is done by showing

2168: that if $A$ is prenex, then there is a formula $A^G$ which is also prenex and

2169: which is valid in $\gdl{V}$ iff $A^g$ is.  Note that not all quantifier

2170: shifting rules are generally valid in Gödel logics, so we have to show that

2171: for the particular case of formulas of the form of $A^g$, there is a prenex

2172: formula which is valid in $\gdl{V}$ iff $A^g$ is.

2173: 

2174: \begin{theorem}

2175: If $V$ is countably infinite, the prenex fragment of $\gdl V$ is not

2176: r.e.

2177: \end{theorem}

2178: 

2179: \begin{proof}

2180: By the proof of Theorem~\ref{thm:count-nonax}, a formula $A$ is true in all

2181: finite models iff $\gdl V \models A^g$.  $A^g$ is of the form $B \impl (A' \lor

2182: \exists u\, P(u))$.  We show that $A^g$ is validity-equivalent in $\gdl V$ to a

2183: prenex formula.

2184: 

2185: % Call a formula $A$ in which every atomic formula occurs negated a

2186: % \emph{classical} formula.  It is easy to see that for any $\I$ and

2187: % $A(x)$ with $\I(A(d)) \in \{0, 1\}$ for all $d$, $\I(\forall x\, A(x)

2188: % \to B) = \I(\exists x\, A(x) \to B)$ and $\I(B \to \exists x\, A(x)) =

2189: % \I(\exists x(B \to A(x))$. 

2190: % Hence, any classical formula is equivalent

2191: % to a prenex formula; 

2192: 

2193: From Lemma~\ref{lm:crisp} we see that each crisp formula is equivalent to a

2194: prenex formula; let $A_0$ be a prenex form of $A'$.  Since all quantifier

2195: shifts for conjunctions are valid, the antecedent~$B$ of $A^g$ is equivalent

2196: to a prenex formula $\Q_1x_1 \ldots \Q_n x_n B_0(x_1, \ldots, x_n)$.  Hence,

2197: $A^g$ is equivalent to $\tup{\Q}\tup{x} B_0(\tup{x}) \to (A_0 \lor \exists u\,

2198: P(u))$.

2199: 

2200: Let $\Q_i'$ be $\exists$ if $\Q_i$ is $\forall$, and $\forall$ if

2201: $\Q_i$ is $\exists$, let $C \equiv A_0 \lor \exists u\, P(u)$, and $v

2202: = \I(\exists u\, P(u)))$.  We show that $\tup{\Q}\tup{x}\,

2203: B_0(\tup{x}) \to C$ is equivalent to $\tup{\Q}'\tup{x}(B_0(\tup{x})

2204: \to C)$ by induction on~$n$.  Let $\tup{\Q}\tup{x}B_0 \equiv \Q_1

2205: x_1\ldots \Q_{i}x_{i} B_1(d_1, \ldots, d_{i-1}, x_i)$.  Since

2206: quantifier shifts for $\exists$ in the antecent of a conditional are

2207: valid, we only have to consider the case $\Q_i = \forall$. Suppose

2208: $\I(\forall x_i\, B_1(\tup{d}, x_i) \impl C) \neq \I(\exists

2209: x_i(B_1(\tup{d}, x_i) \impl C)$. This can only happen if $\I(\forall

2210: x_i\, B_1(\tup{d}, x_i)) = \I(C) < 1$ but $\I(B_1(\tup{d}, c)) > \I(C)

2211: \ge v$ for all $c$.  However, it is easy to see by inspecting $B$ that

2212: $\I(B_1(\tup{d}, c))$ is either $=1$ or $\le v$.

2213: 

2214: Now we show that $\I(B_0(\tup{d}) \impl (A_0 \lor \exists u\, P(u))) =

2215: \I(\exists u(B_0(\tup{d}) \impl (A_0 \lor P(u))))$.  If $\I(A_0) = 1$,

2216: then both sides equal $= 1$.  If $\I(A_0) = 0$, then $\I(A_0 \lor

2217: \exists u\, P(u)) = v$.  The only case where the two sides might

2218: differ is if $\I(B_0(\tup{d})) = v$ but $\I(A_0 \lor P(c)) = \I(P(c))

2219: < v$ for all $c$.  But inspection of $B_0$ shows that $\I(B_0(\tup{t}))

2220: = 1$ or $= \I(P(e))$ for some $e \in \tup{d}$ (the only subformulas of

2221: $B_0(\tup{d})$ which do not appear negated are of the form $e' \prec

2222: e$).  Hence, if $\I(B_0(\tup{d})) = v$, then for some~$e$, $\I(P(e)) =

2223: v$.

2224: 

2225: Last we consider the quantifiers in $A_0 \equiv \tup{\Q} \tup{y}\, A_1$.

2226: Since $A_0$ is crisp, $\I(B_0(\tup{d}) \impl (A_0 \lor P(c))) =

2227: \I(\tup{\Q}\tup{y}(B_0(\tup{d}) \impl (A_1 \lor P(c))))$ for all

2228: $\tup{d}$, $c$.  To see this, first note that shifting quantifiers

2229: across $\lor$, and shifting universal quantifiers out of the

2230: consequent of a conditional is always possible. Hence it suffices to

2231: consider the case of $\exists$.  $\I(\exists y\, A_2)$ is

2232: either $= 0$ or $= 1$.  In the former case, both sides equal

2233: $\I(B_0(\tup{d}) \impl P(d))$, in the latter, both sides equal~$1$.

2234: \end{proof}

2235: 

2236: In summary, we obtain the following characterization of axiomatizability of

2237: prenex fragments of Gödel logics:

2238: 

2239: \begin{theorem}

2240:   The prenex fragment of $\gdl{V}$ is axiomatizable if and only if $V$ is

2241:   finite or uncountable.  The prenex fragments of any two $\gdl{V}$ where $V$

2242:   is uncountable coincide.

2243: \end{theorem}

2244: 

2245: %

2246: % Bottom free fragment

2247: %

2248: 

2249: \subsection{$\bot$-free fragments\label{sec:botfree}}

2250: 

2251: \def\nobot{{\not\bot}}

2252: 

2253: In the following we will denote the $\bot$-free fragment of $\gdl{V}$ with

2254: $\gdl{V}^\nobot$.  $\gdl{V}^\nobot$ is the set of all $\gdl V$-valid formulas

2255: which do not contain $\bot$ (and hence also no $\lnot$).  First we show that

2256: the only candidates for r.e. fragments are the $\bot$-free fragments

2257: of $\gdl V$ where $V$ is uncountable and either $0\in V^\infty$ or $0$ is

2258: isolated~$V$.

2259: 

2260: \begin{lemma}\label{botfree-notra}

2261:   If $\gdl{V}$ is not r.e., then  $\gdl{V}^\nobot$ is also not r.e.

2262: \end{lemma}

2263: 

2264: Define $A^b$ as the formula obtained from $A$ by replacing all occurences of

2265: $\bot$ with the new propositional variable $b$ (a 0-place predicate symbol).

2266: Then define $A^*$ as

2267: \[ 

2268:     A^* = \big(\lAnd_{P\in A}\qa\bar x(b\limp P(\bar x))\big)\limp A^b 

2269: \]

2270: where $P\in A$ means that $P$ ranges over all predicate symbols occuring

2271: in~$A$.  We will first prove a lemma relating $A^*$ and $A$:

2272: 

2273: \begin{lemma}\label{bot-valid}

2274:   \[ \gdl{V} \entails A \quad\text{iff}\quad \gdl{V}^{\nobot} \entails A^* \]

2275: \end{lemma}

2276: \begin{proof}

2277:   If: Replace $b$ by $\bot$.

2278:   

2279:   Only if: Suppose $\gdl{V}^\nobot\nentails A^*$. Thus, there is an

2280:   interpretation $\I_0$ such that $\I_0(A^*) < 1$. By

2281:   Proposition~\ref{fact:loewenheim} and

2282:   Lemma~\ref{lemma:interpretation-cut-off}, there is an interpretation $\I$

2283:   such that $\I(A^b) < 1$ and $\I((\lAnd_{P\in A}\qa\bar x(b\limp P(\bar

2284:   x))))=1$.  Because of the latter, for every atomic subformula~$B$ of $A$,

2285:   $\I(B) \ge \I(b) = v$.  Define $\I'(B)$ for atomic subformulas $B$ of $A$ by

2286:   \[

2287:    \I'(B) = \begin{cases} 0 & \I(B) \le v\\

2288:                        \I(B)& \I(B) > v

2289:              \end{cases}

2290:   \]

2291:   (and arbitrary for other atomic formulas).  It is easily seen by induction

2292:   that $\I'(B) = \I(B)$ if $\I(B) > v$, and if $\I(B) = v$, then $\I'(B) = v$

2293:   or $=0$.  In particular, $\I'(A^b) < 1$.  But, of course, $\I'(b) = \I'(\bot)

2294:   = 0$, and hence $\I'(A^b) = \I'(A)$.

2295: 

2296: %%  and extend $\I'$ as usual to all

2297: %%   formulas. \Frage{Wieso geht das?  ZB: $A$ is $\lnot \forall x\, C(x)$, dann

2298: %%     ist $A^b \equiv \forall x\, C(x) \to b$.  Sagen wir, $\inf C(x) = \I(b)$.

2299: %%     Dann ist $\I(A^b) = 1$ aber $\I'(A^b) = \I'(b) = 0$.  Man muss wohl zeigen

2300: %%   dass $\I'(F) \ge \I(F)$}

2301: 

2302: %%   Below we will prove the following property: If $\I(F)<1$, then

2303: %%   $\I'(F)<1$. Recall the we assumed that 

2304: %%   $\gdl{V}^\nobot\nentails A^*$ and $\I(A^*)<1$, thus we have

2305: %%   $\I'(A^*)<1$ and by easy induction this is $\I'(A)<1$.

2306: 

2307: %%   Proof of the property that $\I(F)<1$ implies that $\I'(F)<1$: For

2308: %%   atomic $Q$ this is trivial from the definition of $\I'$. Assume that

2309: %%   $\I(F\limp G)<1$. Then $1\ge\I(F)>\I(G)$. Using the fact that

2310: %%   $\I(\lAnd_{P\in A}\qa\bar  x(b\limp P(\bar x)))=1$ and the

2311: %%   implication that all interpretations of sub formulas of $A$ are

2312: %%   greater then $\I(b)$ we know that also $\I'(F)>\I'(G)$, thus

2313: %%   $\I'(F\limp G)=\I'(G)<1$. The proof for the other connectives and

2314: %%   the quantifiers is straight formward.

2315: \end{proof}

2316: 

2317: \begin{proof}[Proof of Lemma~\ref{botfree-notra}]

2318:   If $\gdl{V}^\nobot$ were recursively enumerable, then by

2319:   Lemma~\ref{bot-valid}, $\gdl{V}$ would also be recursively

2320:   enumerable. 

2321: \end{proof}

2322: 

2323: Thus, by Theorem~\ref{thm:count-nonax}, we only have two candidates for

2324: axiomatizable $\bot$-free fragments: both truth-value sets have a non-empty

2325: perfect kernel~$P$, and in the one case $0\in P$ and in the other $0\not\in P$

2326: but $0$ is isolated. The prototypical Gödel sets for these cases are

2327: $V_1 = [0,1]$ and $V_2 = \{0\} \cup [1/2,1]$. We will show that the $\bot$-free

2328: fragments of these two logics coincide, thus in fact proving that there is

2329: only one axiomatizable $\bot$-free fragment.

2330: \fxnote{This should be done also for entailment!}

2331: \begin{lemma}\label{embedding-half}

2332:   Let $V_1 = [0,1]$ and $V_2 = \{0\} \cup [1/2,1]$.

2333:   The $\bot$-free fragments of $\gdl{V_1}$ and $\gdl{V_2}$ coincide,

2334:     i.e.\ 

2335:     \[ \gdl{V_1}^\nobot\entails A\quad\text{iff}\quad

2336:        \gdl{V_2}^\nobot\entails A

2337:     \]

2338: \end{lemma}

2339: \begin{proof}

2340:   Only if: obvious, since a counter-example in $V_2$ actually also is a

2341:   counter-example in $V_1$.

2342:   

2343:   If: Suppose that $\gdl{V_1}^\nobot \nentails A$, i.e., there is an

2344:   $\I_1$ such that $\I_1(A)<1$. Define $\I_2$ for all atomic

2345:   subformulas~$B$ of $A$ by $\I_2(B) = 1/2(1+\I_1(B))$. By 

2346:   Lemma~\ref{lem:induced-interpretation} and the remark following it

2347:   we see that the definition of $\I_2$ extends to all formulas.

2348: \end{proof}

2349: 

2350: \begin{theorem}

2351:   The $\bot$-free fragment of $\gdl{V}$ is recursively axiomatizable

2352:   if and only if $V$ is finite or uncountable and either $0$ belongs to

2353:   $V^\infty$ or is isolated.  The $\bot$-free fragment of any two

2354:   such $V$ coincide.

2355: \end{theorem}

2356: \fxnote{We should give the axiomatization}

2357: \begin{proof}

2358:   From Lemma~\ref{botfree-notra}, Lemma~\ref{embedding-half} and

2359:   Theorem~\ref{thm:gs-id} for the

2360:   uncountable case. The finite case is obvious as the additional axioms

2361:   $\axfinn$ do not contain $\bot$.

2362: \end{proof}

2363: 

2364: %

2365: % Existential fragment

2366: %

2367: \subsection{$\forall$-free fragments}\label{sec:efrag}

2368: 

2369: In the following we will denote the $\exists$-fragment of $\gdl{V}$ with

2370: $\gdl{V}^\exists$. It is the set of all formulas valid in $\gdl V$ which do not

2371: contain~$\forall$.

2372: 

2373: First we show, as in the case of the $\bot$-free fragment, that the

2374: only candidates for axiomatizable fragments are the two uncountable

2375: ones, $0\in P$ and $0$ isolated.   We will do this by showing that the

2376: formulas used to reduce validity in the other cases to Trachtenbrodt's Theorem

2377: are validity-equivalent to $\forall$-free formulas.  

2378: 

2379: \begin{lemma}\label{lm:qshift}

2380:   If $A(x)$ and $B$ are $\forall$-free, then

2381:   \[ \entails \qa x\, A(x)\limp B \quad\text{iff}\quad \entails

2382:   \qe x(A(x)\limp B)\]

2383: \end{lemma}

2384: \begin{proof}

2385:   If: This is a valid quantifier shift

2386:   rule. 

2387:   

2388:   Only if: Suppose that $\nentails\qe x(A(x)\limp B)$, i.e., there is an

2389:   interpretation~$\I$ such that $\I(\qe x(A(x)\limp B)<1$. But this implies

2390:   that

2391:   \begin{equation}

2392:     \label{eq:foo}

2393:     \qa u\in U \quad \I(A(u))>\I(B).

2394:   \end{equation}

2395:   Now define $\I'(Q)$ for atomic subformulas~$Q$ of $A$ by 

2396:   \begin{equation*}

2397:     \I'(Q) = \begin{cases}

2398:       \I(Q) & \text{if\ } \I(Q) \le \I(B) \\

2399:       1     & \text{if\ } \I(Q) > \I(B).

2400:     \end{cases}

2401:   \end{equation*}

2402:   Then (i) If $C$ is $\forall$-free and $\I(C) > \I(B)$, then $\I'(C) = 1$,

2403:   and if $\I(C) \le \I(B)$, then $\I'(C) = \I(C)$; and (ii) $\I'(\qa x\,

2404:   A(x)) = 1$

2405:   

2406:   (i) For atomic $C$ this is the definition of $\I'$. The cases for $\land$,

2407:   $\lor$, and $\limp$ are trivial. Now let $C \equiv \qe x\, D(x)$. If $\I(\qe

2408:   x\, D(x)) > \I(B)$, then for some $u \in U^\I$, $\I(D(u)) > \I(B)$. By

2409:   induction hypthesis, $\I'(D(u)) = 1$ and hence $\I'(\qe x\, D(x)) = 1$.

2410:   Otherwise, $\I(\qe x\, D(x)) \le \I(B)$, in which case $\I'(D(u)) =

2411:   \I'(D(u))$ for all $u$.  (ii) By~(\ref{eq:foo}), for all $u\in U$, $\I(A(u))

2412:   > \I(B)$, hence, by (i), $\I'(A(u)) = 1$.

2413:  

2414:   By (i) and~(ii) we have that $\I'(\qa x\, A(x)) = 1$ and

2415:   $\I'(B) = \I(B) < 1$, thus $\I'(\qa x\, A(x) \limp B) < 1$, i.e., $\nentails

2416:   \qa x\, A(x) \limp B$.

2417: \end{proof}

2418: 

2419: Note that in the preceding Lemma we can replace the prefix of $A(x)$

2420: by a string of universal quantifiers and the same proof will work.

2421: 

2422: \begin{lemma}\label{exists-notra}

2423:   If $\gdl{V}$ is not recursively enumerable, then also $\gdl{V}^\exists$.

2424: \end{lemma}

2425: 

2426: \begin{proof}

2427:   It is sufficient to show that Formula~\ref{fm:countable} for

2428:   $A^g$ as given on page~\pageref{fm:countable} and

2429:   Formula~\ref{fm:0notiso} for $A^h$ as given on 

2430:   page~\pageref{fm:0notiso} are validity-equivalent to $\forall$-free formulas.

2431: 

2432:   If we only consider the quantifier structure of these formulas and

2433:   apply valid quantifier shifting rules, including the shifting rule

2434:   for crisp formulas given in Lemma~\ref{lm:crisp}, we obtain in both

2435:   cases formulas which are of the form

2436:   \[ \qa \bar x A(\bar x) \limp B \]

2437:   where $A(\bar x)$ and $B$ are $\forall$-free. By to Lemma~\ref{lm:qshift} we

2438:   see that both formulas are validity equivalent to $\forall$-free formulas.

2439: \end{proof}

2440: 

2441: As for the $\bot$-free fragments, it turns out that the two prototypical

2442: examples of Gödel sets create the same $\exists$-fragment:

2443: 

2444: \begin{lemma}\label{embhalf2}

2445:   Let $V_1 =[0,1]$ and $V_2 =\{0\}\cup[1/2,1]$.  The $\exists$-fragments of

2446:   $\gdl{V_1}$ and $\gdl{V_2}$ coincide, i.e.\ 

2447:   \[ \gdl{V_1}^\exists \entails A \quad\text{iff}\quad

2448:   \gdl{V_2}^\exists \entails A

2449:   \]

2450: \end{lemma}

2451: \begin{proof}

2452:   Only if: obvious, since a counter-example in $V_2$ actually also is a

2453:   counter-example in $V_1$.

2454:   

2455:   If: Suppose that $\gdl{V_1}^\exists \nentails A$, i.e., there is an $\I_1$

2456:   such that $\I_1(A)<1$. Define $\I_2$ for all atomic subformulas~$B$ of $A$

2457:   by $\I_2(B) = 1/2(1+ \I_1(B))$ if $\I_1(B) > 0$ and $= 0$ if $\I_1(Q)=0$.

2458:   By Lemma~\ref{lem:induced-interpretation} and the remark following it

2459:   we see that the definition of $\I_2$ extends to all formulas.

2460: \end{proof}

2461: 

2462: \fxnote{This should be done for entailment if possible}

2463: \begin{theorem}

2464:   The $\exists$-fragment of $\gdl{V}$ is r.e. if and only if $V$ is finite or

2465:   uncountable and either $0$ belongs to $V^\infty$ or is isolated.  The

2466:   $\exists$-fragment of any two such $V$ coincide.

2467: \end{theorem}

2468: \fxnote{We should give a comment on the axiomatization!}

2469: \begin{proof}

2470:   From Lemma~\ref{exists-notra}, Lemma~\ref{embhalf2} and

2471:   Theorem~\ref{thm:gs-id} for the uncountable case. The finite case is obvious

2472:   as the additional axioms $\axfinn$ do not contain universal quantifiers.

2473: \end{proof}

2474: 

2475: 

2476: \section{Conclusion}

2477: 

2478: In the preceding sections, we have given a complete characterization of the

2479: r.e. and non-r.e. first-order Gödel logics.  Our main result is that there are

2480: two distinct r.e. infinite-valued G\"odel logics, viz., $\GR$ and $\Go$.  What

2481: we have not done, however, is investigate how many \emph{non}-r.e. Gödel

2482: logics there are.  It is known that there are continuum-many different

2483: propositional consequence relations and continuum-many different propositional

2484: quantified Gödel logics \cite{BaazVeith99LC}.  In forthcoming work \cite{bgp},

2485: it is shown that there are only countably many first-order Gödel logics.

2486: Although this result goes some way to clarifying the situation, a criterion of

2487: identity of Gödel logics using some topological property of the underlying

2488: truth value set is a desideratum.  We have only given

2489: (Lemma~\ref{lem:g-embed}) a sufficient condition: if there is a continuous

2490: bijection between $V$ and $V'$, then $\gdl{V} = \gdl{V'}$.  But this condition

2491: is not necessary: any pair of non-isomorphic uncountable Gödel sets with $0$

2492: contained in the perfect kernel provides a quick counterexample (as any two

2493: such sets determine~$\GR$ as their logic).  Such a topological

2494: characterization of first-order infinite valued Gödel logics could then be

2495: used to obtain a more fine-grained analysis of the complexity of the non-r.e.

2496: Gödel logics.  As noted already, these also differ in the degree to which they

2497: are non r.e. \cite{Hajek05}.

2498: 

2499: Another avenue for future research would be to carry out the characterization

2500: offered here for extensions of the language.  Candidates for such

2501: extensions are the addition of the projection modalities 

2502: ($\bigtriangleup a = 0$ if $a=1$ and $=1$ if $a <1$), of the

2503: globalization operator of \cite{TT86}, or of the involutive negation 

2504: ($\sim a = 1 - a$).  

2505: It is known that $\GR$ with the addition of these operators is still

2506: axiomatizable.  The presence of the projection modality, in particular,

2507: disturbs many of the nice features we have been able to exploit in this paper,

2508: for instance, in the presence of $\bigtriangleup$ the crucial

2509: Lemma~\ref{lemma:interpretation-cut-off} and

2510: Proposition~\ref{prop:consequences} no longer hold.  Thus, not all of our

2511: results go through for the extended language and new methods will have to be

2512: developed.

2513: 

2514: 

2515: 

2516: \bibliographystyle{alpha}

2517: %\bibliographystyle{bpz}

2518: %\let\H\hungary

2519: \bibliography{bpz}

2520: 

2521: \end{document}

2522: 

2523: 

2524: %%% Local Variables: 

2525: %%% mode: latex

2526: %%% TeX-master: t

2527: %%% End: 

2528: