Metalogic is an open-ended cognitive, formal methodology pertaining to semantics and information processing. The language that mathematizes metalogic is known as metalanguage and deals with metafunctions purely by extension on patterns. A metalogical process involves an effective enrichment in knowledge as logical statements, and, since human cognition is an inherently logic–based representation of knowledge, a metalogical process will always be aimed at developing the scope of cognition by exploring possible cognitive implications reflected on successive levels of abstraction. Indeed, it is (...) basically impracticable to maintain logic–and–metalogic without paying heed to cognitive theorizing. For it is cognitively irrelevant whether possible conclusions are deduced from some premises before the premises are determined to be true or whether the premises themselves are determined to be true first and, then, the conclusions are deduced from them. In this paper we consider the term metalogic as inherently embodied under the framework referred to as cognitive science and mathematics. We propose a metalogical interpretation of Arrow’s impossibility theorem and, to that end, choice theory is understood as a mental course of action dealing with logic and metalogic issues, in which a possible mathematical approach to model a mental course of action is adopted as a systematic operating method. Nevertheless, if we look closely at the core of Arrow’s impossibility theorem in terms of metalogic, a second fundamental contribution to this framework is represented by the Nash equilibrium. As a result of the foregoing, therefore, we prove the metalogical equivalence between Arrow’s impossibility theorem and the existence of the Nash equilibrium. More specifically, Arrow’s requirements correspond to the Nash equilibrium for finite mixed strategies with no symmetry conditions. To demonstrate this proof, we first verify that Arrow’s set and Nash’s set are isomorphic to each other, both sets being under stated conditions of non–symmetry. Then, the proof is completed by virtue of category theory. Indeed, the two sets are categories that correspond biuniquely to one another and, thus, it is possible to define a covariant functor that preserves their mutual structures. According to this, we show the proof–dedicated metalanguage as a precursor to a special equivalence theorem. (shrink)

The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating (...) phases of rule application. Since the logic programming community can generate many examples and many design goals, the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic. (shrink)

Some realists claim that theoretical entities like numbers and electrons are indispensable for describing the empirical world. Motivated by the meta-ontology of Quine, I take this claim to imply that, for some first-order theory T and formula δ(x) such that T ⊢ ∃xδ ∧ ∃x¬δ, where δ(x) is intended to apply to all and only empirical entities, there is no first-order theory T′ such that (a) T and T′ describe the δ:s in the same way, (b) T′ ⊢ ∀xδ, and (...) (c) T′ is at least as attractive as T in terms of other theoretical virtues. In an attempt to refute the realist claim, I try to solve the general problem of nominalizing T (with respect to δ), namely to find a theory T′ satisfying conditions (a)–(c) under various precisifications thereof. In particular, I note that condition (a) can be understood either in terms of syntactic or semantic equivalence, where the latter is strictly stronger than the former. The results are somewhat mixed. On the positive side, even under the stronger precisification of (a), I establish that (1) if the vocabulary of T is finite, a nominalizing theory can always be found that is recursive if T is, and (2) if T postulates infinitely many δ:s, a nominalizing theory can always be found that is no more computationally complex than T. On the negative side, even under the weaker precisification of (a), I establish that (3) certain finite theories cannot be nominalized by a finite theory. (shrink)

We discuss the many aspects and qualities of the number one: the different ways it can be represented, the different things it may represent. We discuss the ordinal and cardinal natures of the one, its algebraic behaviour as a neutral element and finally its role as a truth-value in logic.

We try to explain Tarski's conception of logical notions, as it emerges from alecture of his, delivered in 1966 and published posthumously in 1986 (Historyand Philosophy of Logic 7, 143–154), a conception based on the idea ofinvariance. The evaluation of Tarski's proposal leads us to consider an interesting(and neglected) reply to Skolem in which Tarski hints at his own point of view onthe foundations of set theory. Then, comparing the lecture of 1966 with Tarski'slast work and with an earlier paper (...) written with Lindenbaum, it is shown thatTarski's conception of logical notions, with its essentially type-theoretic character,did not undergo any significant modifications throughout his life. A remark onTarski's prudential attitude on the topic in the famous paper on the concept oflogical consequence (and elsewhere) concludes our paper. (shrink)