Abstract
A derealistic, system-free approach, with an example: arithmetic.
For André
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Which also proves \(\mathtt {x}\in \mathbb {N}\multimap \mathtt {\overline{0}} \le \mathtt {x}\), hence .
References
Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76, 95–120 (1988)
Danos, V., Regnier, L.: The structure of multiplicatives. Arch. Math. Logic 28, 181–203 (1989)
Girard, J.-Y.: Une extension de l’interprétation fonctionnelle de Gödel à l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Fenstad (ed.) Proceedings of the 2nd Scandinavian Logic Symposium, pp. 63–92. North-Holland, Amsterdam (1971)
Girard, J.-Y.: Transcendental syntax 1: deterministic case. Mathematical Structures in Computer Science, pp. 1–23 (2015). Computing with lambda-terms. A special issue dedicated to Corrado Böhm for his 90th birthday
Girard, J.-Y.: Transcendental syntax 3: equality. Logical Methods in Computer Science (2016). Special issue dedicated to Pierre-Louis Curien for his 60th birthday
Girard, J.-Y., Scedrov, A., Scott, P.: Bounded linear logic: a modular approach to polynomial time computability. Theor. Comput. Sci. 97, 1–66 (1992)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. LFCS report series, Edinburgh, 162 (1991)
Kreisel, G.: Mathematical logic. In: Saaty, T.L. (ed.) Lectures in Modern Mathematics, vol III, pp. 99–105. Wiley, New York (1965)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A L’usine, Again
A L’usine, Again
Usine vs. usage, it’s Church vs Curry. The existentialist approach of Curry is quite respected by the notion of behaviour. On the other hand, the essentialism inherent to the typing à la Church leads to systems and must be deeply modified. I propose the following:
A type (Church style) is a (finite) battery of tests.
This is compatible with polymorphism: several batteries may be used to “type” the same design. However, there is a problem, the definition seeming not to apply in full generality, because of the absence of finite preorthogonals.
I propose the following solution: instead of a preorthognal of behaviour \(\mathbf {P}\), a preorthogonal of a sub-behaviour of \(\mathbf {P}\). Orthogonality to such a preorthogonal need not be necessary, it is only sufficient. On the other hand, it may remain finite, hence the possibility of a battery of tests. Let us give two examples.
1.1 A.1 Identity
The principle \(A \;\mathbin {\vdash }A\), the identity “axiom”, poses a problem of finiteness. It is tested through simultaneous tests, for \(\mathop {\sim }A\) and A, which is possible in certain cases, but doesn’t work in general.
Let us suppose that A correspond to general behaviour \(\mathbf {A}\), with not finiteness restriction. I still know how to justify \(\mathbin {\vdash }\mathop {\sim }A, A\) because it is sufficient to test it against generic pairs, that of a test for \(\mathop {\sim }\mathbf {A}\) and for \(\mathbf {A}\) with no reference to \(\mathbf {A}\) which therefore takes the moral value of a variable X. We know that the cases:
do suffice. They force the presence of a star \(\llbracket \, \mathop {\sim }A(x),A(x) \,\rrbracket \), if I abusively denote the respective locations of \(\mathop {\sim }A\) and A by \(\mathop {\sim }A(x),A(x)\). This implies in turn that the said star does belong to the behaviour \(\mathbin {\vdash }\mathop {\sim }A, A\).
These tests are not necessary: if \(A = B \otimes C\) and \(\mathbin {\vdash }\mathop {\sim }A, A\) has been obtained by “\(\eta \)-expansion” from \(\mathbin {\vdash }\mathop {\sim }B, B\) and \(\mathbin {\vdash }\mathop {\sim }C, C\), they fail.
We just witnessed the native sufficient testing. Remark that its two parts are not independent: if A is tested as , \(\mathop {\sim }A\) must be tested as .
1.2 A.2 Existence
Existence can be informally reduced to a very peculiar case, that of the implication \(\forall X\,A \mathbin {\vdash }A[T/X]\), in other terms \(\mathbin {\vdash }\exists X\,\mathop {\sim }A, A[T/X]\). We must test \((\mathcal {T,T',P})\) where \(\mathcal {P}\) is the identity \(\mathbin {\vdash }\mathop {\sim }A[T/X], A[T/X]\). We just observed that this identity possesses a sufficient battery of tests. We conclude that \(\mathcal {P}\) belongs to the behaviour associated with \(\mathbin {\vdash }\mathop {\sim }A[T/X], A[T/X]\).
In order to show that \((\mathcal {T,T',P})\) is in the behaviour (7) corresponding to \(\mathbin {\vdash }\exists X\,\mathop {\sim }A, A[T/X]\), we imitate the argument given for system \(\mathbb {F}\): the comprehension principle shows that the behaviour associated with T is a set, and we use the “substitution lemma” of [3].
1.3 A.3 Finitism
The finitistic pattern advocated by Hilbert is correct provided we throw in some necessary distinctions. Three layers are needed:
-
Usine: Typing à la Church, but system-free. It enables us to predict the behaviour are doing.
-
Usage: Typing à la Curry, naturally system-free. A behavourial approach, what proofs are actually doing.
-
Adequation: Cut-elimination, so to speak. It shows the accuracy of the prediction of l’usine.
The first two layers are the opposite sides of finitism, of a completely different nature. The first person who (vaguely) understood the distinction was Lewis Carroll (1893), who mistook l’usine for the “meta” of l’usage and built a ludicrous wild goose chase which he dared compare with Zeno’s paradox. Indeed, by replacing a cut on A with a cut on \(A \Rightarrow A\), next a cut on \((A \Rightarrow A)\Rightarrow (A\Rightarrow A)\), etc. Carroll’s Achilles is constantly fleeing away from the Tortoise... no wonder it never reaches him.
The third layer, adequation, does not belong to finitism: it is where an infinitary, eventually set-theoretic, argument must be thrown in... with no possible way of bypassing it.
vitam impendere logicæ
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Girard, JY. (2020). Transcendental Syntax iv: Logic Without Systems. In: Nigam, V., et al. Logic, Language, and Security. Lecture Notes in Computer Science(), vol 12300. Springer, Cham. https://doi.org/10.1007/978-3-030-62077-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-030-62077-6_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-62076-9
Online ISBN: 978-3-030-62077-6
eBook Packages: Computer ScienceComputer Science (R0)