Search

We sharpen Hajek’s Completeness Theorem for theories extending predicate product logic, $${\Pi\forall}$$ . By relating provability in this system to embedding properties of ordered abelian groups we construct a universal BL-chain L in the sense that a sentence is provable from $${\Pi\forall}$$ if and only if it is an L-tautology. As well we characterize the class of lexicographic sums that have this universality property.

In the paper we introduce a wide range of Anderson-like variants of Godel's theory and prove for each of them strong completeness theorem wrt. corresponding class of modal structures. These theories — all formulated in the 2nd order modal language with a 2nd order unary predicate of positiveness — differ among themselves with respect of: properties of the necessity operator and of the predicate of positiveness, axioms characterizing identity between 1st sort terms, definitions of identity between 2nd sort terms, the treatment of Godlikeness as a term of the 2nd order, the treatment of necessary existence as a term of the 2nd order if there exists the necessity of its presence, the treatment of Ix (Ix(y) is read: terms x, y are identical), for every 1st sort term x, as a term of the 2nd order if there exists the necessity of its presence. Concerning to semantical commitments, the following are essential: (i) 1st order terms order receive only rigid extensions in the constant objectual 1st order domain; (ii...

We investigate the deduction problem in Godel and Product logics, both equipped with Godel negation, in the countable case. Our approach is based on translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. An order clause is a finite set of order literals of the form \(\varepsilon _1\diamond \varepsilon _2\) where \(\diamond \) is a connective either Open image in new window or \(\prec \). Open image in new window and \(\prec \) are interpreted by th xe equality and standard strict linear order on [0, 1], respectively. We generalise the well-known hyperresolution principle to the standard first-order Godel logic and devise a calculus operating over order clausal theories. A variant of the DPLL procedure in the propositional Product logic exploiting trichotomy and operating over order clausal theories, will be proposed. Both the calculi are refutation sound and complete for the countable case.

We analyze a class of modal logics rendered insensitive to reflexivity by way of a modification to the semantic definition of the modal operator. We explore the extent to which these logics can be characterized, and prove a general completeness theorem on the basis of a translation between normal modal logics and their reflexive-insensitive counterparts. Lastly, we provide a sufficient semantic condition describing when a similarly general soundness result is also available.

In this paper we study input/output STIT logic. We introduce the semantics, proof theory and prove the completeness theorem. Input/output STIT logic has more expressive power than Makinson and van der Torre’s input/output logic. We show that input/output STIT logic is decidable and free from Ross’ paradox.

This paper discusses the problem of availability of constructive metamathematics for constructive theories. Since intuitionism is usually considered as the most important kind of constructivism, we have the following question: Is it possible to give intuitionistically acceptable proofs of metamathematical theorems? This issue is illustrated by the completeness theorem for intuitionistic predicate logic and the consistency of arithmetic. The conclusion is that hitherto collected evidence justifies the claim that the universal intuitionistic metamathematics is very problematic.

In the paper Justification logics and hybrid logics, Melvin Fitting initiated the idea of combining justification logics and hybrid logics into a single system. However, for some technical reason, he presented a basic-hybrid justification logic \(\mathsf {JT}\) instead of \(\mathsf {J}\) with proving completeness theorem and realization theorem. The task of weakening this logic to \(\mathsf {J}\) was left as an open problem in conclusion. This paper aims at solving this problem to further facilitate the proof of the properties of this logic as well as the derivation of other members of this logic family.

In the paper, we generalise the well-known hyperresolution principle to the standard first-order Godel logic. Our approach is based on the translation of a formula of Godel logic to an equivalent satisfiable finite order clausal theory, consisting of order clauses. We introduce a notion of quantified atom: a formula a is a quantified atom iff a = Q x p(t 0,…,t τ ) where Q is a quantifier (∀, ∃); p(t 0,…,t τ ) is an atom; x is a variable occurring in p(t 0,…,t τ ); for all i ≤ τ, either t i = x or x does not occur in t i . Then an order clause is a finite set of order literals of the form e 1 ⋄ e 2 where e i is either an atom or a quantified atom, and ⋄ is a connective either \(\eqcirc \) or ≺. \(\eqcirc \) and ≺ are interpreted by the equality and strict linear order on [0,1], respectively. For an input theory of Godel logic, the proposed translation produces a so-called admissible order clausal theory. On the basis of the hyperresolution principle, a calculus operating over admissible order clausal theories, is devised. The calculus is proved to be refutation sound and complete for the countable case.

This paper considers Henkin’s proof of completeness of classical first-order logic and extends its scope to the realm of algebraizable logics in the sense of Blok and Pigozzi. Given a propositional logic L (for which we only need to assume that it has an algebraic semantics and a suitable disjunction) we axiomatize two natural first-order extensions L∀m and L∀ and prove that the former is complete with respect to all models over algebras from , while the latter is complete with respect to all models over relatively finitely subdirectly irreducible algebras. While the first completeness result is relatively straightforward, the second requires non-trivial modifications of Henkin’s proof by making use of the disjunction connective. As a byproduct, we also obtain a form of Skolemization provided that the algebraic semantics admits regular completions. The relatively modest assumptions on the propositional side allow for a wide generalization of previous approaches by Rasiowa, Sikorski, Hájek, Horn, and others and help to illuminate the “essentially first-order” steps in the classical Henkin’s proof.

Defeasible conditionals of the form ‘if A then normally B’ are usually interpreted with the aid of a ‘normality’ ordering between possible states of affairs: \(A\Rightarrow B\) is true if it happens that in the most ‘normal’ (least exceptional) A-worlds, B is also true. Another plausible interpretation of ‘normality’ introduced in nonmonotonic reasoning dictates that \(A\Rightarrow B\) is true iff B is true in ‘most’ A-worlds. A formal account of ‘most’ in this majority-based approach to default reasoning has been given through the usage of (weak) filters and (weak) ultrafilters, capturing at least, a basic core of a size-oriented approach to defeasible reasoning. In this paper, we investigate defeasible conditionals constructed upon a notion of ‘overwhelming majority’, defined as ‘truth in a cofinite subset of \(\omega \)’, the first infinite ordinal. One approach employs the modal logic of the frame \((\omega

Wansing's extended intuitionistic linear logic with strong negation, called WILL, is regarded as a resource-conscious refinment of Nelson's constructive logics with strong negation. In this paper, (1) the completeness theorem with respect to phase semantics is proved for WILL using a method that simultaneously derives the cut-elimination theorem, (2) a simple correspondence between the class of Petri nets with inhibitor arcs and a fragment of WILL is obtained using a Kripke semantics, (3) a cut-free sequent calculus for WILL, called twist calculus, is presented, (4) a strongly normalizable typed ?-calculus is obtained for a fragment of WILL, and (5) new applications of WILL in medical diagnosis and electric circuit theory are proposed. Strong negation in WILL is found to be expressible as a resource-conscious refutability, and is shown to correspond to inhibitor arcs in Petri net theory.

In the present paper the idea of Wang [G.J. Wang, Theory of truth degrees of formulas in Łukasiewicz n-valued propositional logic and a limit theorem, Sci. China Inform. Sci. E 35(6) (2005) 561–569 (in Chinese)] is firstly extended to the n-valued R0-logic L n ∗ and the concept of truth degrees of formulas in L n ∗ is proposed. A limit theorem saying that the truth function τn induced by truth degrees converges to the integrated truth function τ when n converges to infinity is obtained. This theorem builds a bridge between discrete valued R0-logic and continuous valued R0-logic. Secondly, based on deduction theorem, completeness theorem and the concept of truth degrees of formulas in L n ∗ , the concept of consistency degrees of theories is given. It is proved that a theory Γ over L n ∗ is a useless theory(i.e., the deductions of Γ are all tautologies) iff the consistency degree consistn(Γ) of Γ is equal to 1, Γ is consistent iff 1 2 ⩽ consist n ( Γ ) ⩽ 1 , and Γ is inconsistent iff consistn(Γ) = 0. Lastly, the concept of consistency degrees of theories is generalized and a method of graded reasoning in L n ∗ is obtained.

An infinitary proof theory is developed for modal logics whose models are coalgebras of polynomial functors on the category of sets. The canonical model method from modal logic is adapted to construct a final coalgebra for any polynomial functor. The states of this final coalgebra are certain “maximal” sets of formulas that have natural syntactic closure properties.The syntax of these logics extends that of previously developed modal languages for polynomial coalgebras by adding formulas that express the “termination” of certain functions induced by transition paths. A completeness theorem is proven for the logic of functors which have the Lindenbaum property that every consistent set of formulas has a maximal extension. This property is shown to hold if the deducibility relation is generated by countably many inference rules.A counter-example to completeness is also given. This is a polynomial functor that is not Lindenbaum: it has an uncountable set of formulas that is deductively consistent but has no maximal extension and is unsatisfiable, even though all of its countable subsets are satisfiable.

A topological class logic is an infinitary logic formed by combining a first-order logic with the quantifier symbols O and C. The meaning of a formula closed by quantifier O is that the set defined by the formula is open. Similarly, a formula closed by quantifier C means that the set is closed. The corresponding models are a topological class spaces introduced by Ciric and Mijajlovic (Math Bakanica 1990). The completeness theorem is proved.

We give resource bounded versions of the Completeness Theorem for propositional and predicate logic. For example, it is well known that every computable consistent propositional theory has a computable complete consistent extension. We show that, when length is measured relative to the binary representation of natural numbers and formulas, every polynomial time decidable propositional theory has an exponential time (EXPTIME) complete consistent extension whereas there is a nondeterministic polynomial time (NP) decidable theory which has no polynomial time complete consistent extension when length is measured relative to the binary representation of natural numbers and formulas. It is well known that a propositional theory is axiomatizable (respectively decidable) if and only if it may be represented as the set of infinite paths through a computable tree (respectively a computable tree with no dead ends). We show that any polynomial time decidable theory may be represented as the set of paths through a polynomial time decidable tree. On the other hand, the statement that every polynomial time decidable tree represents the set of complete consistent extensions of some theory which is polynomial time decidable, relative to the tally representation of natural numbers and formulas, is equivalent to P = NP. For predicate logic, we develop a complexity theoretic version of the Henkin construction to prove a complexity theoretic version of the Completeness Theorem. Our results imply that that any polynomial space decidable theory Δ possesses a polynomial space computable model which is exponential space decidable and thus Δ has an exponential space complete consistent extension. Similar results are obtained for other notions of complexity.

This paper is a contribution to the development of model theory of fuzzy logic in narrow sense. We consider a formal system EvŁ of fuzzy logic that has evaluated syntax, i. e. axioms need not be fully convincing and so, they form a fuzzy set only. Consequently, formulas are provable in some general degree. A generalization of Godel's completeness theorem does hold in EvŁ. The truth values form an MV-algebra that is either finite or Łukasiewicz algebra on [0, 1]. The classical omitting types theorem states that given a formal theory T and a set Σ(x1, … , xn ) of formulas with the same free variables, we can construct a model of T which omits Σ, i. e. there is always a formula from Σ not true in it. In this paper, we generalize this theorem for EvŁ, that is, we prove that if T is a fuzzy theory and Σ(x1, … , xn ) forms a fuzzy set , then a model omitting Σ also exists. We will prove this theorem for two essential cases of EvŁ: either EvŁ has logical (truth) constants for all truth values, or it has these constants for truth values from [0, 1] ∩ ℚ only. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π02. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's Theorem.

As it was shown in Jenei and Montagna (Studia Logica 70(2): 183---192, 2002), Monoidal t-norm based logic (MTL) is a logic of left-continuous t-norms. In other words, this means that MTL enjoys the standard completeness theorem. In this paper we present a different proof of this theorem. In fact, we prove even more since we show that MTL is complete w.r.t. the class of standard MTL-algebras with finite congruence lattice or equivalently with finitely many Archimedean classes. We also show the connection between the congruence lattice of an MTL-chain and its Archimedean classes.

Após uma breve resenha da vida de Gödel, assinalando as origens de suas tradições intelectuais, são analisados o seu teorema da completude, o seu trabalho de tese, o teorema da incompletude e o teorema sobre a impossibilidade de demonstrar a consistência de sistemas formais complexos dentro do mesmo sistema formal. A seguir, são discutidas suas contribuições à independência da Hipótese do Contínuo e do Axioma de Escolha dos outros axiomas da teoria dos conjuntos. Nesse contexto são finalmente discutidas algumas idéias em relação à pequena influência que as contribuições de Gödel, para descrever alguns dos limites do pensamento racional, têm tido nas assim chamadas ciências exatas ou naturais, especialmente, Física e Química. Algumas reflexões são, nesse sentido, propostas.

We study the variety of Lob algebras , the algebraic structures associated with formal propositional calculus. Among other things, we prove a completeness theorem for formal propositional logic with respect to the variety of Lob algebras. We show that the variety of Lob algebras has the weak amalgamation property. Some interesting subclasses of the variety of Lob algebras, e.g. linear, faithful and strongly linear Lob algebras are introduced. (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a ''trace'' any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.

In this paper we define a model theory and give a semantic proof of cut-elimination for ICTT, an intuitionistic formulation of Church's theory of types defined by Miller et al. and the basis for the λProlog programming language. Our approach, extending techniques of Takahashi and Andrews and tableaux machinery of Fitting, Smullyan, Nerode and Shore, is to prove a completeness theorem for the cut-free fragment and show semantically that cut is a derived rule. This allows us to generalize a result of Takahashi and Schutte on extending partial truth valuations in impredicative systems. We extend Andrews' notion of Hintikka sets to intuitionistic higher-order logic in a way that also defines tableau-provability for intuitionistic type theory. In addition to giving a completeness theorem without using cut we then show, using cut, how to establish completeness of more conventional term models. These models give a declarative semantics for the logic underlying the λProlog programming language.

The logic just corresponding to (non-commutative) involutive quantales, which was introduced by Wendy MacCaull, is reconsidered in order to obtain a cut-free sequent calculus formulation, and the completeness theorem (with respect to the involutive quantale model ) for this logic is proved using a new admissible rule. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

A new basis for making logical inference in inconsistent systems is considered. Main inference rules and the completeness theorem (in narrow sense) of the calculus proposed are proved. The approach proposed can underlie the creation of systems of substantiation of inconsistent and unreliable solutions obtained, for instance, in designing intelligent robots and expert systems.

Logic of proofs L P introduced by S. Artemov in 1995 describes properties of proof predicate 't is a proof of F' in the propositional language extended by atoms of the form [[t]]F. Proof are represented by terms constructed by three elementary recursive operations on proofs. In order to make the language more expressive we introduce the additional storage predicate with the intended interpretation 'x is a label for F'. It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments. In this paper we study operations on proofs and labels that can be specified in the extended language. First, we give a formal definition of an operation on proofs and labels. Then, for an arbitrary finite set of operations F the logic L P S(F) is defined. We provide L P S(F) with symbolic semantics and arithmetical semantics. The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.

The paper presents generalizations of results on so-called Horn logic, well-known in universal algebra, to the setting of fuzzy logic. The theories we consider consist of formulas which are implications between identities (equations) with premises weighted by truth degrees. We adopt Pavelka style: theories are fuzzy sets of formulas and we consider degrees of provability of formulas from theories. Our basic structure of truth degrees is a complete residuated lattice. We derive a Pavelka-style completeness theorem (degree of provability equals degree of truth) from which we get some particular cases by imposing restrictions on the formulas under consideration. As a particular case, we obtain completeness of fuzzy equational logic.

Gödel has emphasized the important role that his philosophical views had played in his discoveries. Thus, in a letter to Hao Wang of December 7, 1967, explaining why Skolem and others had not obtained the completeness theorem for predicate calculus, Gödel wrote:This blindness (or prejudice, or whatever you may call it) of logicians is indeed surprising. But I think the explanation is not hard to find. It lies in a widespread lack, at that time, of the required epistemological attitude toward metamathematics and toward non-finitary reasoning. …I may add that my objectivist conception of mathematics and metamathematics in general, and of transfinite reasoning in particular, was fundamental also to my other work in logic.How indeed could one think of expressing metamathematics in the mathematical systems themselves, if the latter are considered to consist of meaningless symbols which acquire some substitute of meaning only through metamathematics?Or how could one give a consistency proof for the continuum hypothesis by means of my transfinite model Δ if consistency proofs have to be finitary?In a similar vein, Gödel has maintained that the “realist” or “Platonist” position regarding sets and the transfinite with which he is identified was part of his belief system from his student days. This can be seen in Gödel's replies to the detailed questionnaire prepared by Burke Grandjean in 1974. Gödel prepared three tentative mutually consistent replies, but sent none of them.

This paper will formulate and offer evidence for a conjecture on the analytical behaviour of residual Eisenstein series in the positive Weyl chamber. It should play a major role in an also conjectural Paley-Wiener theorem about the Schwartz space of arithmetic quotients. If things work out as I expect, this development should be logically independent of Chapter 7 of [Langlands:1976], and in the end one should obtain a new proof of Langlands’ completeness theorem.

A schematic extension NMŁ of F.Esteva and L.Godo's Logic MTL is introduced in this paper. Based on a new left-continuous but discontinuous t-norm, which was proposed by S.Jenei and can be regarded as a kind of distorted nilpotent minimum, the semantics of NMŁ is interpreted and the standard completeness theorem of NMŁ is proved. The fact that the maximum and the minimum are definable from the negation and implication in NMŁ and NM is discovered, which also leads to a modification of the NM axiom system.

We prove a full completeness theorem for multiplicative–additive linear logic (i.e. MALL ) using a double gluing construction applied to Ehrhard’s *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free MALL proof. Our proof consists of three steps. We show: • Dinatural transformations on this category satisfy Joyal’s softness property for products and coproducts. • Softness, together with multiplicative full completeness, guarantees that every dinatural transformation corresponds to a Girard MALL proof-structure. • The proof-structure associated with any dinatural transformation is a MALL proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures. The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences.

It is shown that Cech completeness, ultra completeness and local compactness can be defined by demanding that certain equivalences hold between certain lasses of Baire measures or by demanding that certain lasses of Baire measures have non-empty support. This shows that these three topological properties are measurable, similarly to the classical examples of compact spaces, pseudo-compact spaces and real compact spaces., peer-reviewed

Quasi-equational logic concerns with a completeness theorem, i. e. a list of general syntactical rules such that, being given a set of graded quasi-equations Q, the closure Cl Q = Qeq Fun Q can be derived from \(Q \subseteq (X:QE)\) by the given rules. Those rules do exist, because our consideration could be embedded into the logic of first order language. But, we look for special (“quasi-equational”) rules. Suitable rules were already established for the (non-functorial) case of partial algebras in Definition 3.1.2 of [27], p. 108, and [28], p. 102. (For the case of total algebras, see [35].) So, one has to translate these rules to the (functorial) language of partial theories \(\underline T \in \left| {\underline {\mathcal{T}h} } \right|\).

We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for object-oriented sequential programming. For the sake of concreteness, and because of practical relevance, we consider objects using message exchange to implement method invocation and overriding. The main contribution of the paper is an intersection type assignment system, obtained by a combination of systems introduced for the Calculus of Mobile Ambients and for the &-calculus. We exploit in the mobility framework a typical feature of the intersection type discipline for object calculi, namely late typing of self. The proposed system is then checked against standard properties of related systems, establishing type invariance and a completeness theorem.

Intervals in boolean algebras enter into the study of conditional assertions (or events) in two ways: directly, either from intuitive arguments or from Goodman, Nguyen and Walker's representation theorem, as suitable mathematical entities to bear conditional probabilities, or indirectly, via a representation theorem for the family of algebras associated with de Finetti's three-valued logic of conditional assertions/events. Further representation theorems forge a connection with rough sets. The representation theorems and an equivalent of the boolean prime ideal theorem yield an algebraic completeness theorem for the three-valued logic. This in turn leads to a Henkin-style completeness theorem. Adequacy with respect to a family of Kripke models for de Finetti's logic, Łukasiewicz's three-valued logic and Priest's Logic of Paradox is demonstrated. The extension to first-order yields a short proof of adequacy for Korner's logic of inexact predicates.

ΠMTL is a schematic extension of the monoidal t-norm based logic (MTL) by the characteristic axioms of product logic. In this paper we prove that ΠMTL satisfies the standard completeness theorem. From the algebraic point of view, we show that the class of ΠMTL-algebras (bounded commutative cancellative residuated l-monoids) in the real unit interval [0,1] generates the variety of all ΠMTL-algebras.

We initiate the study of computable model theory of modal logic, by proving effective completeness theorems for a variety of first-order modal logics. We formulate a natural definition of a decidable Kripke model, and show how to construct such a decidable Kripke model of a given decidable theory. Our construction is inspired by the effective Henkin construction for classical logic. The Henkin construction, however, depends in an essential way on the Deduction Theorem. In its usual form the Deduction Theorem fails for modal logic. In our construction, the Deduction Theorem is replaced by a result about objects called finite Kripke diagrams. We argue that this result can be viewed as an analogue of the Deduction Theorem for modal logic.

In 1691 Michel Rolle (1652–1719) first published his famous result, now widely known as ‘Rolle's theorem’, in an obscure book on geometry and algebra, named Methode pour resoudre les egalites. Jose...

In a previous work with Antonio Bucciarelli, we introduced indexed linear logic as a tool for studying and enlarging the denotational semantics of linear logic. In particular, we showed how to define new denotational models of linear logic using symmetric product phase models (truth-value models) of indexed linear logic. We present here a strict extension of indexed linear logic for which symmetric product phase spaces provide a complete semantics. We study the connection between this new system and indexed linear logic.

In Girard (2001), J.-Y. Girard presents a new theory, The Ludics, which is a model of realisibility of logic that associates proofs with designs, and formulas with behaviours. In this article we study the interpretation in this semantics of formulas with first-order quantifications and their proofs. We extend to the first-order quantifiers the full completeness theorem obtained in Girard (2001) for $MALL_2$. A significant part of this article is devoted to the study of a uniformity property for the families of designs that represent proofs of formulas depending on a first-order free variable.

We investigate the notion of substitution in an abstract way, without defining it explicitly. We single out the essential features of the operation of performing a substitution in order to define a concept of substitutive structure. called logos. We then prove a completeness theorem making precise and justifying the intuition that formulas true for the usual substitution can be proved from the logos axioms only. (C) 2004 Academie des sciences. Publie par Elsevier SAS. Tous droits reserves.

A full separation theorem for the derivable rules of intuitionistic linear logic without bounds, 0 and exponentials is proved. Several structural consequences of this theorem for subreducts of (commutative) residuated lattices are obtained. The theorem is then extended to the logic LR+ and its proof is extended to obtain the finite embeddability property for the class of square increasing residuated lattices.

We consider a concept of substitutive structure, called "logos", in order to study simple substitution, independently of formal or programming languages. We provide a definition of simultaneous substitution in an arbitrary logos and use it to prove a completeness theorem expressing that the equational properties of the usual substitution can be proved from the logos axioms only.

The theory that ``consistency implies existence'' was put forward by Hilbert on various occasions around the start of the last century, and it was strongly and explicitly emphasized in his correspondence with Frege. Since (Godel's) completeness theorem, abstractly speaking, forms the basis of this theory, it has become common practice to assume that Hilbert took for granted the semantic completeness of second order logic. In this paper I maintain that this widely held view is untrue to the facts, and that the clue to explain what Hilbert meant by linking together consistency and existence is to be found in the role played by the completeness axiom within both geometrical and arithmetical axiom systems.

The concept of fibring is extended to higher-order logics with arbitrary modalities and binding operators. A general completeness theorem is established for such logics including HOL and with the meta-theorem of deduction. As a corollary, completeness is shown to be preserved when fibring such rich logics. This result is extended to weaker logics in the cases where fibring preserves conservativeness of HOL-enrichments. Soundness is shown to be preserved by fibring without any further assumptions.

We present the dual to Birkhoff's variety theorem in terms of predicates over the carrier of a cofree coalgebra (that is, in terms of ‘coequations’). We then discuss the dual to Birkhoff's completeness theorem, showing how closure under deductive rules dualises to yield two modal operators acting on coequations. We discuss the properties of these operators and show that they commute. We prove as our main result the invariance theorem, which is the formal dual of Birkhoff's completeness theorem.

We present the first complete problem for SZK, the class of promise problems possessing statistical zero-knowledge proofs (against an honest verifier). The problem, called Statistical Difference, is to decide whether two efficiently samplable distributions are either statistically close or far apart. This gives a new characterization of SZK that makes no reference to interaction or zero knowledge .We propose the use of complete problems to unify and extend the study of statistical zero knowledge. To this end, we examine several consequences of our Completeness Theorem and its proof, such as:---A way to make every (honest-verifier) statistical zero-knowledge proof very communication efficient, with the prover sending only one bit to the verifier (to achieve soundness error 1/2).---Simpler proofs of many of the previously known results about statistical zero knowledge, such as the Fortnow and Aiello--Hεstad upper bounds on the complexity of SZK and Okamoto's result that SZK is closed under complement.---Strong closure properties of SZK that amount to constructing statistical zero-knowledge proofs for complex assertions built out of simpler assertions already shown to be in SZK.---New results about the various measures of "knowledge complexity," including a collapse in the hierarchy corresponding to knowledge complexity in the "hint" sense.---Algorithms for manipulating the statistical difference between efficiently samplable distributions, including transformations that "polarize" and "reverse" the statistical relationship between a pair of distributions.

In this paper I deal with first order logic and axiomatic systems. I present the metalogical results that show the property of satisfying Modus Ponens as a necessary and sufficient condition for the extended completeness of the system, and to the Deduction Metatheorem as a necessary and sufficient condition for the extended correctness of the system. Both supposing that the system satisfies the corresponding restricted properties. These results show that the choice of that rule of inference and of that metatheorem, for any particular axiomatic system, are not a matter of personal liking or of practical convenience, but they play a fundamental role for the extended correctness-completeness properties of the axiomatic system. As a matter of fact, they can be considered as structural properties that characterize the fulfilling of the Extended Correctness and Completeness theorem for the axiomatic system.