Off-campus access
Using PhilPapers from home?
Click here to configure this browser for off-campus access.
- Jaroslav Peregrin, Inferentializing Semantics.The whole development of modern logic is marked by various forms of confrontation of what has come to be called proof theory with what has earned the label of model theory. The heart of theories of systems of formal logic are usually considered to be proofs of soundness and (in)completeness - in effect results concerning the relationship between proof-theoretically delimited theorems and model-theoretically delimited tautologies. Those founding fathers of modern logic who saw logic as primarily a matter of rules, people like Frege, Peano or Russell, articulated the most basic axiomatic systems of logic, thus putting the concept of proof on a firm foundation. Thereafter Hilbert set up proof theory as an ambitious program based on the mathematical investigation of arithmetized proofs, aimed at showing consistency, independence and completeness of axiomatic systems by the perspicuous means of elementary arithmetic, and consequently reducing mathematics to the investigation of provability of its statements (See Kreisel, 1964 and 1968). In the thirties, Gentzen (1934; 1936) showed that proof theory need not rest on the concept of axiomatic system, but put forward the systems of natural deduction and sequent calculi (which are not based on inferring sentences from sentences, but, in effect, rather instances of inference from instances of inference). Recently, proof theory has come to be understood as a wholly general investigation of proofs and proof systems, often carried out in ways that are more algebraic than arithmetical (see Buss, 1998). However, the thirties witnessed also the spectacular demonstration of limitations of proof theory - viz. Gödel's proof of the impossibility of reaching all truths of arithmetic (not to speak about more complicated systems) by means of proof theory. This led to a revival of semantic methods in logic, due especially to Alfred Tarski (1933, 1936, 1939) and his school. (A semantic strand was, to be sure, present throughout the whole development of modern logic ever before Tarski, thanks to logicians who came to logic from algebra, i.e..No categoriesIn my reading list | Discuss this article | Edit | Categorize |My bibliography
| Export citation | Scholar
Discussion of Jaroslav Peregrin, Inferentializing semantics
Nothing in this forum yet.
Similar books and articles
Although resolution-based inference is perhaps the industry standard in automated theorem proving, there have always been systems that employed a different format. For example, the Logic Theorist of 1957 produced proofs by using an axiomatic system, and the proofs it generated would be considered legitimate axiomatic proofs; Wang’s systems of the late 1950’s employed a Gentzen-sequent proof strategy; Beth’s systems written about the same time employed his semantic tableaux method; and Prawitz’s systems of again about the same time are often (...)
In my reading list
| Discuss this article | Edit | Categorize | My bibliography | Export citation | Other links: sfu.ca springerlink.com | Scholar | More..
| | Other links: sfu.ca springerlink.com | Scholar | More.. This paper is concerned with real proofs as opposed to formal proofs, and specifically with the ultimate reason of real proofs (‘Why Proof?’) and with the notion of real proof (‘What is a Proof?’). Several people believed and still believe that real proofs can be represented by formal proofs. There are various reasons for thinking that this belief is unjustified. To discuss this matter one must answer the questions: Why proof? What is a proof? In this paper these questions are (...)
No categories
In my reading list
| Discuss this article | Edit | Categorize | My bibliography | Export citation | Other links: w3.uniroma1.it | Scholar | More..
| | Other links: w3.uniroma1.it | Scholar | More.. This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.
This book presents an up-to-date, unified treatment of research in bounded arithmetic and complexity of propositional logic, with emphasis on independence proofs and lower bound proofs. The author discusses the deep connections between logic and complexity theory and lists a number of intriguing open problems. An introduction to the basics of logic and complexity theory is followed by discussion of important results in propositional proof systems and systems of bounded arithmetic. More advanced topics are then treated, including polynomial simulations and (...)
Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.
Linear logic is a new logic which was recently developed by Girard in order to provide a logical basis for the study of parallelism. It is described and investigated in Gi]. Girard's presentation of his logic is not so standard. In this paper we shall provide more standard proof systems and semantics. We shall also extend part of Girard's results by investigating the consequence relations associated with Linear Logic and by proving corresponding str ong completeness theorems. Finally, we shall investigate (...)
Proof, Logic and Formalization addresses the various problems associated with finding a philosophically satisfying account of mathematical proof. It brings together many of the most notable figures currently writing on this issue in an attempt to explain why it is that mathematical proof is given prominence over other forms of mathematical justification. The difficulties that arise in accounts of proof range from the rightful role of logical inference and formalization to questions concerning the place of experience in proof and the (...)
No categories
Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof be replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic (the so-called Rosser logic of Gauspari-Solovay, 1979) so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in (...)
Our aim is to express in exact terms the old idea of solving problems by pure questioning. We consider the problem of derivability: Is A derivable from by classical propositional logic?. We develop a calculus of questions E *; a proof (called a Socratic proof) is a sequence of questions ending with a question whose affirmative answer is, in a sense, evident. The calculus is sound and complete with respect to classical propositional logic. A Socratic proof in E * can (...)
Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural logics. The book (...)
