Logic prototyping: approach and use cases

In this article, we present an approach to prototyping complex systems and processes using classical predicate logic. The prototype is built by the interpreter based on a logical description of the properties and/or behavior of the designed system. The description contains the definitions of the prototype elements and the constraints that the correct prototype must satisfy. Definitions are used to build a prototype, and constraints are used to analyze it and check the required properties. Definitions are interpreted using direct logic inference, constraints are only checked on the resulting model. A wider class of formulas is used than in well-known logical languages. Computable logical and denotational semantics are defined for them. In the process of building a prototype, logical errors of uncertainty, redefinition of functions, and contradictions are diagnosed. We are given examples of prototype descriptions used for semantic program analysis, space training, transport system design.

Natural deduction

Natural deduction is a philosophically as well as pedagogically important logical proof system. This chapter introduces Gerhard Gentzen’s original system of natural deduction for minimal, intuitionistic, and classical predicate logic. Natural deduction reflects the ways we reason under assumption in mathematics and ordinary life. Its rules display a pleasing symmetry, in that connectives and quantifiers are each governed by a pair of introduction and elimination rules. After providing several examples of how to find proofs in natural deduction, it is shown how deductions in such systems can be manipulated and measured according to various notions of complexity, such as size and height. The final section shows that the axiomatic system of classical logic presented in Chapter 2 and the system of natural deduction for classical logic introduced in this chapter are equivalent.

Undecidability of the Logic of Partial Quasiary Predicates

We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the non-theorem. Therefore, we also obtain an embedding of the classical predicate logic of finite models into the logic of partial quasiary predicates over finite structures. As a consequence, we prove that the logic of partial quasiary predicates is undecidable—more precisely, $\varSigma ^0_1$-complete—over arbitrary structures and not recursively enumerable—more precisely, $\varPi ^0_1$-complete—over finite structures.

LOGIC FOR THE THEORY OF CONCEPTS

In this paper, we follow Gödel’s remarks on an envisioned theory of concepts to determine which properties should a logical basis of such a theory have. The discussion is organized around the question of suitability of the classical predicate calculus for this role. Some reasons to think that classical logic is not an appropriate basis for the theory of concepts, will be presented. We consider, based on these reasons, which alternative logical system could fare better as a logical foundation of, in Gödel’s opinion, the most important theory in logic yet to be developed. This paper should, in particular, motivate the study of partial predicates in a certain system of three-valued logic, as a promising starting point for the foundation of the theory of concepts.

Elementary-base cirquent calculus II: Choice quantifiers

Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of $\textbf{CL17}$ augments that of $\textbf{CL16}$ by including choice quantifiers. Unlike classical predicate calculus, $\textbf{CL17}$ turns out to be decidable.

Free logics, philosophical issues in

The expression ‘free logic’ is a contraction of the more cumbersome ‘logic free of existence assumptions with respect to both its general terms (predicates) and its singular terms’. Its most distinctive feature is the rejection of the principle of universal specification, a principle of classical predicate logic which licenses the logical truth of statements such as ‘If everything rotates then (the planet) Mars rotates’. If a free logic contains the general term ‘exists’, this principle is replaced by a restricted version, one which licenses the logical truth only of statements such as ‘If everything rotates then Mars rotates, provided that Mars exists’. If the free logic does not contain the general term ‘exists’, but contains the term ‘is the same as’, the principle is replaced by a version which licenses only statements such as ‘If everything rotates then Mars rotates, provided that there is an object the same as Mars’. Most free logicians regard the restricted version of universal specification as simply making explicit an implicit assumption, namely, that Mars exists. Indeed, free logic is the culmination of a long historical trend to rid logic of existence assumptions with respect to its terms. Just as classical predicate logic purports to be free of the hidden existence assumptions which pervaded the medieval theory of inference with respect to its general terms, so free logic rids classical predicate logic of hidden existence assumptions with respect to its singular terms. There are various kinds of free logic, with many interesting and novel philosophical applications. These cover a wide range of issues from the philosophy of mathematics to the philosophy of religion. In addition to the issue of how to analyse singular existence statements, of the form ‘3 + 7 exists’ and ‘That than which nothing greater can be conceived exists’, of special importance are issues in the theory of definite descriptions, set theory, the theory of reference, modal logic and the theory of complex general terms.

On the Definitional Embeddability of the Combinatory Logic Theory into the First-Order Predicate Calculus

In this article we prove a theorem on the definitional embeddability of the combinatory logic into the first-order predicate calculus without equality. Since all efficiently computable functions can be represented in the combinatory logic, it immediately follows that they can be represented in the first-order classical predicate logic. So far mathematicians studied the computability theory as some applied theory. From our theorem it follows that the notion of computability is purely logical. This result will be of interest not only for logicians and mathematicians but also for philosophers who study foundations of logic and its relation to mathematics.