Transcendental Syntax iv: Logic Without Systems

A derealistic, system-free approach, with an example: arithmetic.

1. 1.

   Which also proves \(\mathtt {x}\in \mathbb {N}\multimap \mathtt {\overline{0}} \le \mathtt {x}\), hence .

Authors and Affiliations

1. Directeur de Recherches émérite, Marseille, France

   Jean-Yves Girard

Corresponding author

Correspondence to Jean-Yves Girard .

Editors and Affiliations

1. fortiss GmbH, Munich, Germany

   Vivek Nigam

2. University of Rijeka, Rijeka, Croatia

   Tajana Ban Kirigin

3. SRI International, Menlo Park, CA, USA

   Carolyn Talcott

4. Worcester Polytechnic Institute, Worcester, MA, USA

   Joshua Guttman

5. Steklov Mathematical Institute of the Russian Academy of Sciences, Moscow, Russia

   Stepan Kuznetsov

6. University of Pennsylvania, Philadelphia, PA, USA

   Boon Thau Loo

7. Keio University, Tokyo, Japan

   Mitsuhiro Okada

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:

(23)

(24)

(25)

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æ

Reprints and permissions

© 2020 Springer Nature Switzerland AG

Policies and ethics