The Gödel–Artemov framework offered a formalization of the Brouwer–Heyting–Kolmogorov semantics of intuitionistic logic via classical proofs. In this framework, the intuitionistic propositional logic IPC is embedded in the modal logic S4, S4 is realized in the Logic of Proofs LP, and LP has a provability interpretation in Peano Arithmetic. Self-referential LP-formulas of the type ‘t is a proof of a formula ϕ containing t itself’ are permitted in the realization of S4 in LP, and if such (...) formulas are indeed involved, it is then necessary to use fixed-point arithmetical methods to explain intuitionistic logic via provability. The natural question of whether self-referentiality can be avoided in realization of S4 was answered negatively by Kuznets who provided an S4-theorem that cannot be realized without using directly self-referential LP-formulas. This paper studies the question of whether IPC can be embedded in S4 and then realized in LP without using self-referential formulas. We consider a general class of Gödel-style modal embeddings of IPC in S4 and by extending Kuznetsʼ method, show that there are IPC-theorems such that, under each such embedding, are mapped to S4-theorems that cannot be realized in LP without using directly self-referential formulas. Interestingly, all double-negations of tautologies that are not IPC-theorems, like ¬¬, are shown to require direct self-referentiality. Another example is found in IPC→, the purely implicational fragment of IPC. This suggests that the BHK semantics of intuitionistic logic is intrinsically self-referential. (shrink)

It is widely accepted that there is a clear sense in which the first-order paraconsistent constructive logic with strong negation of Almukdad and Nelson, QN4, is more constructive than intuitionistic first-order logic, QInt. While QInt and QN4 both possess the disjunction property and the existence property as characteristics of constructiveness (or constructivity), QInt lacks certain features of constructiveness enjoyed by QN4, namely the constructible falsity property and the dual of the existence property. This paper deals with the constructiveness of the (...) contra-classical, connexive, paraconsistent, and contradictory non-trivial first-order logic QC, which is a connexive variant of QN4. It is shown that there is a sense in which QC is even more constructive than QN4. The argument focuses on a problem that is mirror-inverted to Raymond Smullyan’s drinker paradox, namely the invalidity of what will be called the drinker truism and its dual in QN4 (and QInt), and on a version of the Brouwer-Heyting-Kolmogorov interpretation of the logical operations that treats proofs and disproofs on a par. The validity of the drinker truism and its dual together with the greater constructiveness of QC in comparison to QN4 may serve as further motivation for the study of connexive logics and suggests that constructive logic is connexive and contradictory (the latter understood as being negation inconsistent). (shrink)

In this paper it is argued that the understanding of Brouwer as replacing truth conditions with assertability or proof conditions, in particular as codified in the so-called Brouwer-Heyting-Kolmogorov Interpretation, is misleading and conflates a weak and a strong notion of truth that have to be kept apart to understand Brouwer properly: truth-as-anticipation and truth- in-content. These notions are explained, exegetical documentation provided, and semi-formal recursive definitions are given.

Straightforwardly and strictly intuitionistic inferences show that the Brouwer– Heyting–Kolmogorov interpretation, in the presence of a formulation of the recognition principle, entails the validity of the Law of Testability: that the form ¬ f V ¬¬ f is valid. Therefore, the BHK and recognition, as described here, are inconsistent with the axioms both of intuitionistic mathematics and of Markovian constructivism. This finding also implies that, if the BHK and recognition are suitably formulated, then Brouwer’s original (...) weak counterexample reasoning was fallacious. The results of the present article extend and refine those of McCarty, C.. Antirealism and Constructivism: Brouwer’s Weak Counterexamples. The Review of Symbolic Logic. First View. Cambridge University Press. (shrink)

We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the intuitionistic (...) and co-intuitionistc sides of polarized bi-intuitionism. Philosophically, we extend Dalla Pozza and Garola’s pragmatic interpretation of intuitionism as a logic of assertions [10] to bi-intuitionism as a logic of assertions and hypotheses. We focus on the logical role of illocutionary forces and justification conditions in order to provide “intended interpretations” of logical systems that classify inferential uses in natural language and remain acceptable from an intuitionistic point of view. Although Dalla Pozza and Garola originally provide a constructive interpretation of intuitionism in a classical setting, we claim that some conceptual refinements suffice to make their “pragmatic interpretation” a bona fide representation of intuitionism. We sketch a meaning-asuse interpretation of co-intuitionism that seems to fulfil the requirements of Dummett and Prawitz’s justificationist approach. We extend the Brouwer-Heyting-Kolmogorov interpretation to bi-intuitionism by regarding co-intuitionistic formulas as types of the evidence for them: if conclusive evidence is needed to justify assertions, only a scintilla of evidence suffices to justify hypotheses. (shrink)

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.

Artemov and Protopopescu introduced a Brouwer-Heyting-Kolmogorov interpretation of knowledge operator to define the intuitionistic epistemic logic IEL, where the axiom A⊃KA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$A\supset KA$$\end{document} is accepted but the axiom KA⊃A\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$KA\supset A$$\end{document} is refused. This paper studies the notion of distributed knowledge on an expansion of the multi agent variant of IEL. We provide a BHK interpretation of distributed knowledge operator (...) to define the intuitionistic epistemic logic with distributed knowledge DIEL. We construct Hilbert system and cut-free sequent calculus for DIEL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathbf {DIEL}$$\end{document} and show that they are sound and complete for the intended Kripke semantics. (shrink)

ABSTRACT In 1933 Gödel introduced an axiomatic system, currently known as S4, for a logic of an absolute provability, i.e. not depending on the formalism chosen ([God 33]). The problem of finding a fair provability model for S4 was left open. The famous formal provability predicate which first appeared in the Gödel Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with S4. As was discovered in [Art 95], this defect of the formal provability (...) predicate can be bypassed by replacing hidden quantifiers over proofs by proof polynomials in a certain finite basis. The resulting Logic of Proofs enjoys a natural arithmetical semantics and provides an intended provability model for S4, thus answering a question left open by Gödel in 1933. Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer- Heyting- Kolmogorov interpretation, ?-calculus and modal ?-calculus. In the current paper we demonstrate how the intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown, that Int is complete with respect to this proof realizability. (shrink)

Intuitionistic epistemic logic by Artemov and Protopopescu (Rev Symb Log 9:266–298, 2016) accepts the axiom “if A, then A is known” (written $$A \supset K A$$ ) in terms of the Brouwer–Heyting–Kolmogorov interpretation. There are two variants of intuitionistic epistemic logic: one with the axiom “ $$KA \supset \lnot \lnot A$$ ” and one without it. The former is called $$\textbf{IEL}$$, and the latter is called $$\textbf{IEL}^{-}$$. The aim of this paper is to study first-order expansions (...) (with equality and function symbols) of these two intuitionistic epistemic logics. We define Hilbert systems with additional axioms called geometric axioms and sequent calculi with the corresponding rules to geometric axioms and prove that they are sound and complete for the intended semantics. We also prove the cut-elimination theorems for both sequent calculi. As a consequence, the disjunction property and existence property are established for the sequent calculi without geometric implications. Finally, we establish that our sequent calculi can also be formulated with admissible structural rules (i.e., in terms of a G3-style sequent calculus). (shrink)

In this paper, we suggest the broader concept of proof-event, introduced by Joseph Goguen, as a fundamental methodological tool for studying proofs in history of mathematics. In this framework, proof is understood not as a purely syntactic object, but as a social process that involves at least two agents; this highlights the communicational aspect of proving. We claim that historians of mathematics essentially study proof-events in their research, since the mathematical proofs they face in the extant sources involve many informal (...) components, often not completely formalizable, and convey some kind of semantic content calling for understanding and verification. We illustrate the application of this methodological approach in some outstanding historical cases, paying particular attention to the process of proof interpretation that makes a proof-event alive. Finally, we suggest a classification of proof-events, according to the conditions imposed upon problem-solving. This enables us to speak about broad classes of proof-events in history of mathematics that share a common characteristic. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As (...) argued in previous work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

I propose a new semantics for intuitionistic logic, which is a cross between the construction-oriented semantics of Brouwer-Heyting-Kolmogorov and the condition-oriented semantics of Kripke. The new semantics shows how there might be a common semantical underpinning for intuitionistic and classical logic and how intuitionistic logic might thereby be tied to a realist conception of the relationship between language and the world.

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics (...) for Int which resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

We outline an intuitionistic view of knowledge which maintains the original Brouwer–Heyting–Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view coreflectionA→KAis valid and the factivity of knowledge holds in the formKA→ ¬¬A‘known propositions cannot be false’.We show that the traditional form of factivityKA→Ais a distinctly classical principle which, liketertium non datur A∨ ¬A, does not hold intuitionistically, but, along with (...) the whole of classical epistemic logic, is intuitionistically valid in its double negation form ¬¬(KA¬A).Within the intuitionistic epistemic framework the knowability paradox is resolved in a constructive manner. We argue that this paradox is the result of an unwarranted classical reading of constructive principles and as such does not have the consequences for constructive foundations traditionally attributed it. (shrink)

In a recent paper by Tranchini (Topoi, 2019), an introduction rule for the paradoxical proposition ρ∗ that can be simultaneously proven and disproven is discussed. This rule is formalized in Martin-Löf’s constructive type theory (CTT) and supplemented with an inferential explanation in the style of Brouwer-Heyting-Kolmogorov semantics. I will, however, argue that the provided formalization is problematic because what is paradoxical about ρ∗ from the viewpoint of CTT is not its provability, but whether it is a proposition (...) at all. (shrink)

On the intended interpretation of intuitionistic logic, Heyting's Proof Interpretation, a proof of a proposition of the form p -> q consists in a construction method that transforms any possible proof of p into a proof of q. This involves the notion of the totality of all proofs in an essential way, and this interpretation has therefore been objected to on grounds of impredicativity (e.g. Gödel 1933). In fact this hardly ever leads to problems as in (...) proofs of implications usually nothing more is assumed about a proof of the antecedent than that it indeed is one, and this assumption does not require a further grasp of the totality of proofs. The prime example of an intuitionistic theorem that goes beyond that assumption is Brouwer's proof of the 'bar theorem': For every tree x, if x contains a decidable subset of nodes such that every path through the tree meets it (a 'bar'), then there is a well-ordered subtree of x that contains a bar for the whole of x. Instantiated with an arbitrary tree t, this proposition takes the form P(t) -> Q(t). Brouwer's proof of the bar theorem mainly consists in an analysis of the inner structure that a proof of P(t) must have, where proofs are taken to be primarily mental objects. So here Brouwer engages in phenomenological reflection by considering the acts in which we think about bars. From that analysis he obtains the information from which to construct a proof of Q(t). In this talk I will argue that Brouwer circumvents the problem of impredicativity by resorting to a transcendental argument based on phenomenological description, and defend this application by showing how common objections to transcendental arguments do not apply here. Finally, I will indulge in some historical speculation by relating the foregoing considerations to the remarkable change that Gödel's view on the Proof Interpretation underwent between his Yale Lecture (1941) and the Dialectica paper (1958). (shrink)

There are two different ways to introduce the notion of truthin constructive mathematics. The first one is to use a Tarskian definition of truth in aconstructive (meta)language. According to some authors, (Kreisel, van Dalen, Troelstra ... ),this definition is entirely similar to the Tarskian definition of classical truth (thesis A).The second one, due essentially to Heyting and Kolmogorov, and known as theBrouwer–Heyting–Kolmogorov interpretation, is to explain informally what it means fora mathematical proposition to be constructively (...) proved. According to other authors (Martin-Löfand Shapiro), this interpretation and the Tarskian definition of truth amount to thesame (thesis B). My aim in this paper is to show that thesis A is only reasonable, that thesis Bis false and to answer the following question: what is defined by the Tarskian definition ofconstructive truth? (shrink)

The term verificationism is used in two different ways: the first is in relation to the verification principle of meaning, which we usually and rightly associate with the logical empiricists, although, as we now know, it derives in reality from Wittgenstein, and the second is in relation to the theory of meaning for intuitionistic logic that has been developed, beginning of course with Brouwer, Heyting and Kolmogorov in the twenties and early thirties, but in much more detail (...) lately, particularly in connection with intuitionistic type theory. It is therefore very natural to ask how these two forms of verificationism are related to one another: was the verificationism that we had in the thirties a kind of forerunner of what we have now, or was it something entirely different? I would like to discuss this question by considering a very particular problem, which was at the heart of Schlick’s interests, namely, the problem whether there might exist undecidable propositions or, if you prefer, unsolvable problems or unanswerable questions: it is merely a matter of wording which of these terms you choose. As I said, it is a problem which was at the heart of Schlick’s interests: it is explicitly discussed already in his early, programmatic paper Die Wende in der Philosophie in the first volume of Erkenntnis from 1930, and there is a short late paper, which has precisely Unanswerable Questions? as its title, from 1935, and he discussed it on several occasions in between also. (shrink)

We define and investigate Heyting-valued interpretations for Constructive Zermelo–Frankel set theory . These interpretations provide models for CZF that are analogous to Boolean-valued models for ZF and to Heyting-valued models for IZF. Heyting-valued interpretations are defined here using set-generated frames and formal topologies. As applications of Heyting-valued interpretations, we present a relative consistency result and an independence proof.

Brouwer’s view on induction has relatively recently been characterised as one on which it is not only intuitive (as expected) but functional, by van Dalen. He claims that Brouwer’s ‘Ur-intuition’ also yields the recursor. Appealing to Husserl’s phenomenology, I offer an analysis of Brouwer’s view that supports this characterisation and claim, even if assigning the primary role to the iterator instead. Contrasts are drawn to accounts of induction by Poincaré, Heyting, and Kreisel. On the phenomenological side, (...) the analysis provides an alternative to that in Tieszen’s Mathematical Intuition, and confirms a view of Gödel on his Dialectica Interpretation. (shrink)

Brouwer’s intuitionism was a far-reaching attempt to reform the foundations of mathematics. While the mathematical community was reluctant to accept Brouwer’s work, its response to later-developed brands of intuitionism, such as those presented by Hermann Weyl and Arend Heyting, was different. The paper accounts for this difference by analyzing the intuitionistic versions of Brouwer, Weyl, and Heyting in light of a two-tiered model of the body and image of mathematical knowledge. Such a perspective provides a (...) richer account of each story and points to a possible connection between the community’s reaction and the changes each mathematician had proposed. (shrink)

I argue against the interpretation of propositions as intentions and proof-objects as fulfillments proposed by Heyting and defended by Tieszen and van Atten. The idea is already a frequent target of criticisms regarding the incompatibility of Brouwer’s and Husserl’s positions, mainly by Rosado Haddock and Hill. I raise a stronger objection in this paper. My claim is that even if we grant that the incompatibility can be properly dealt with, as van Atten believes it can, two fundamental (...) issues indicate that the interpretation is unsustainable regardless: (1) it is hard to determine, without appealing to propositional intentions on pain of circularity, what intention a proof-object should be understood as a fulfillment of; (2) due to a difficult fulfillment dilemma, it is unclear, at best, what the object of an intention corresponding to a proposition is. (shrink)

In one of his essays on art, Dutch author and essayist Joost Zwagerman reflects on the work of South African artist Marlene Dumas. Zwagerman addresses in particular Dumas' My Mother Before She Became My Mother, painted 3 years after her mother died. In his reflections, Zwagerman proposes an interpretation of Dumas' work. He suggests that Dumas, in her art, does not accept the omnipotence of death. Maybe against better judgement, but Dumas keeps creating images that not only illustrate the (...) desire for meaning but also embody this desire. The image and the desire for meaning merge in Dumas' paintings. The painting itself becomes an autonomous 'desire machine', according to Zwagerman. In this article, a theological reading of Zwagerman's own posthumously published volume of poetry, 'Wakend over God', is presented, with a specific interest in art, death and God. The sacramental hermeneutics of Richard Kearney and the theopoetics of John Caputo are brought into the conversation to elicit the dimensions of faith and religion in Zwagerman's own 'desire machine'. (shrink)

The theory of collective agency and intentionality is a flourishing field of research, and our understanding of these phenomena has arguably increased greatly in recent years. Extant theories, however, are still ill-equipped to explain certain aspects of collective intentionality. In this article we draw attention to two such underappreciated aspects: the failure of the intentional states of collectives to supervene on the intentional states of their members, and the role of non-human factors in collective agency and intentionality. We propose a (...) theory of collective intentionality which builds on the ‘interpretationist’ tradition in metasemantics and the philosophy of mind as initiated by David Lewis and recently developed further by Robbie Williams. The collective-level analogue of interpretationism turns out to look different in some ways from the individual-level theory, but is well-suited to accommodating phenomena such as hybrid collective intentionality. Complemented with Kit Fine’s theory of variable embodiment, such a theory also provides a diachronic account of intentional collectives. (shrink)

Ten years ago, researchers using event-related brain potentials to study language comprehension were puzzled by what looked like a Semantic Illusion: Semantically anomalous, but structurally well-formed sentences did not affect the N400 component—traditionally taken to reflect semantic integration—but instead produced a P600 effect, which is generally linked to syntactic processing. This finding led to a considerable amount of debate, and a number of complex processing models have been proposed as an explanation. What these models have in common is that they (...) postulate two or more separate processing streams, in order to reconcile the Semantic Illusion and other semantically induced P600 effects with the traditional interpretations of the N400 and the P600. Recently, however, these multi-stream models have been called into question, and a simpler single-stream model has been proposed. According to this alternative model, the N400 component reflects the retrieval of word meaning from semantic memory, and the P600 component indexes the integration of this meaning into the unfolding utterance interpretation. In the present paper, we provide support for this “Retrieval–Integration ” account by instantiating it as a neurocomputational model. This neurocomputational model is the first to successfully simulate the N400 and P600 amplitude in language comprehension, and simulations with this model provide a proof of concept of the single-stream RI account of semantically induced patterns of N400 and P600 modulations. (shrink)

Grotius's notion of natural law is, as he himself makes clear, founded upon two demands of nature, which are to be connected with what is now known as the Stoic doctrine of appropriation. However, Grotius's understanding of the notion of natural law as a set of rules is not Stoic, but rather goes back to an interpretation that can be ascribed to Antiochus of Ascalon. By moving away from the Stoics Grotius could not only easily accommodate the Aristotelian doctrine (...) of equity, otherwise rejected by the Stoics, but he could also formulate a minimalistic interpretation of human dispositions or 'rights', in contrast to the Stoics' maximalistic understanding of these dispositions as virtues. (shrink)

How can philosophy exert its critical function in society and in education if any appeal to independent and even relatively ‘certain’ criteria seems problematic? The epistemological doubts that foundationalist models of justification encounter unavoidably seem to raise this question. In particular, the relativist implications that seem to result from rejecting such models seem to paralyse the critical potential of philosophy of education. In order to explore the possibilities of a conception of educational critique that avoids the pitfalls of foundationalism, I (...) analyse the epistemological dimensions of this much-feared relativism, illustrating this with some characteristic examples. Solving the problems raised will require an interpretation of critique that leaves our daily sense of critique intact, without literally adopting its—foundationalist—basic assumptions. After systematically developing such an alternative interpretation of critical usage, a non-relativist but still non-foundationalist and powerful conception of philosophical critique seems possible. I illustrate results with some examples from philosophy of education. (shrink)

The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance, minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc. The isomorphism has many aspects, even at the syntactic level: formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to (...) term reduction, etc. But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transforms proofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq). This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic. Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme. · Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics. · Elaborate study of classical logics and control operators. · Account of dialogue games for classical and intuitionistic logic. · Theoretical foundations of computer-assisted reasoning. (shrink)

The classical interpretation of mathematical statements can be seen as comprising two separate but related aspects: a domain and a truth-schema. L. E. J. Brouwer’s intuitionistic project lays the groundwork for an alternative conception of the objects in this domain, as well as an accompanying intuitionistic truth-schema. Drawing on the work of Arend Heyting and Michael Dummett, I present two objections to classical mathematical semantics, with the aim of creating an opening for an alternative interpretation. With (...) this accomplished, I then make the case for intuitionism as a suitable candidate to fill this void. (shrink)

This book is the first collection of essays in English devoted solely to the relationship between Aristotle’s ethics and politics. Are ethics and politics two separate spheres of action or are they unified? Those who support the unity-thesis emphasize the centrality for Aristotle of questions about the good life and the common good as the purpose of politics. Those who defend the separation-thesis stress Aristotle’s sense of realism in understanding the need for political solutions to human shortcomings. But is this (...) all there is to it? The contributors to this volume explore and develop different arguments and interpretative frameworks that help to make sense of the relationship between Aristotle’s Ethics and Politics. The chapters loosely follow the order of the Nicomachean Ethics in examining topics such as political science, statesmanship and magnanimity, justice, practical wisdom, friendship, and the relationship between the active and the contemplative life. They have in common an appreciation of the relevance of Aristotle’s writings, which offer the modern reader distinct philosophical perspectives on the relationship between ethics and politics. (shrink)

Many philosophers of education emphasise the impossibility to really ‘solve’ philosophical—and with that, educational—problems these days. Philosophers have been trying to give philosophy a new, constructive turn in the face of this insolvability. This paper focuses on irony-based approaches that try to exploit the very uncertainty of philosophical issues to further philosophical understanding. We will first briefly discuss a few highlights of historical uses of irony as a philosophical tool. Then we concentrate on two different interpretations of irony, formulated by (...) Bransen and Rorty, that aim at gaining insight into how we make meaning of the world, while at the same time recognising that such an understanding would be impossible. After discussing some problematic aspects of these interpretations a third interpretation of irony is developed, based on a third view of the nature of meaning-making. Following these three interpretations, we will discuss their philosophical merits and the different kinds of insight they can produce for philosophy of education. (shrink)

Many philosophers of education emphasise the impossibility to really ‘solve’ philosophical—and with that, educational—problems these days. Philosophers have been trying to give philosophy a new, constructive turn in the face of this insolvability. This paper focuses on irony-based approaches that try to exploit the very uncertainty of philosophical issues to further philosophical understanding. We will first briefly discuss a few highlights of historical uses of irony as a philosophical tool. Then we concentrate on two different interpretations of irony, formulated by (...) Bransen and Rorty, that aim at gaining insight into how we make meaning of the world, while at the same time recognising that such an understanding would be impossible. After discussing some problematic aspects of these interpretations a third interpretation of irony is developed, based on a third view of the nature of meaning-making. Following these three interpretations, we will discuss their philosophical merits and the different kinds of insight they can produce for philosophy of education. (shrink)

In this paper we introduce a logic that we name semi Heyting–Brouwer logic, \, in such a way that the variety of double semi-Heyting algebras is its algebraic counterpart. We prove that, up to equivalences by translations, the Heyting–Brouwer logic \ is an axiomatic extension of \ and that the propositional calculi of intuitionistic logic \ and semi-intuitionistic logic \ turn out to be fragments of \.

Constructive mathematics is based on the thesis that the meaning of a mathematical formula is given, not by its truth-conditions, but in terms of what constructions count as a proof of it. However, the meaning of the terms 'construction' and 'proof' has never been adequately explained (although Kreisel, Goodman and Martin-Löf have attempted axiomatisations). This monograph develops precise (though not wholly formal) definitions of construction and proof, and describes the algorithmic substructure underlying intuitionistic logic. Interpretations of Heyting arithmetic and (...) constructive analysis are given. The philosophical basis of constructivism is explored thoroughly in Part I. The author seeks to answer objections from platonists and to reconcile his position with the central insights of Hilbert's formalism and logic. Audience: Philosophers of mathematics and logicians, both academic and graduate students, particularly those interested in Brouwer and Hilbert; theoretical computer scientists interested in the foundations of functional programming languages and program correctness calculi. (shrink)

This book is an attempt to relate the operative and constructive formulation of symbolic logic carried out by Lorenzen—and to a lesser degree Kolmogorov and Markov—to both Wittgenstein's philosophy of logic as set forth in the Tractatus and later modified in the Investigations, and to Brouwer's critique of classical logic, especially the principles of excluded middle. The first chapter contains an exposition of Wittgenstein's critical analysis of the "mythical" views of Russell and Frege; and it develops his own (...) "operative" theory of elementary logic. The second chapter concerns the relations of the theories of Brouwer and Wittgenstein; the last section is a detailed survey of chiefly Lorenzen's operative logic in which the presentation of a dialogue-like interpretation of logic is exhaustively analyzed: the notion of a "winning strategy" in such a two-person dialogue is set forth, the technique is extended to classical logic from its original, weaker operational form, and its relations to Gentzen's Sequenzen-kalkül is discussed. The work was the author's Habilitationsschrift at Innsbruck University.—P. J. M. (shrink)

We compare the elementary theories of Shannon information and Kolmogorov complexity, the extent to which they have a common purpose, and wherethey are fundamentally different. We discuss and relate the basicnotions of both theories: Shannon entropy, Kolmogorov complexity, Shannon mutual informationand Kolmogorov (``algorithmic'') mutual information. We explainhow universal coding may be viewed as a middle ground betweenthe two theories. We consider Shannon's rate distortion theory, whichquantifies useful (in a certain sense) information.We use the communication of information as (...) our guiding motif, and we explain howit relates to sequential question-answer sessions. (shrink)

La littérature témoigne d’une tendance croissante à soutenir l’intuitionisme par la phénoménologie. Le disciple de Brouwer Arend Heyting est considéré comme un précurseur de cette tendance, parce qu’il usait d’une terminologie phénoménologique en vue de définir la négation intuitioniste, en élaborant la première logique intuitioniste. Dans cet article, l’auteur tente d’explorer — en référence aux matériaux inédits conservés aux Archives Heyting — ce qui, dans la pensée de Heyting, est compatible avec la phénoménologie. Dans la conclusion, (...) l’auteur suggère que Heyting et Husserl, pour autant qu’ils pensent tous deux que la conscience doit être le véritable commencement de la connaissance, partagent une même attitude antipsychologiste coexistant avec une tentative de dépassement du solipsisme. Toutefois, le concept phénoménologique de degré d’évidence ne peut être appliqué à l’échelle de l’évidence de Heyting (incluant les petits nombres naturels, les grands nombres naturels, les suites infinies, le quantificateur universel), d’un côté parce qu’on ne voit pas clairement si la seconde est partagée par tous les intuitionistes, et de l’autre parce que le premier présuppose une évidence révisable qui ne cadre pas avec le point de vue de Heyting. En outre, les conceptions de la nature de la mathématique et de la logique et de leurs relations mutuelles défendues par Husserl et Heyting sont essentiellement différentes. D’un point de vue intuitioniste, la mathématique est le domaine de l’évidence, alors que la logique transcrit ses régularités. D’un point de vue phénoménologique, la mathématique demeure en dehors du domaine de l’évidence. La logique apophantique coïncide avec la mathématique (sans que l’une absorbe l’autre), mais la logique transcendantale se situe à un niveau plus élevé. (shrink)