A unifying semantics for logic
by
Claudio Sossai
ISIB-CNR, Padova, Italy

In logic there are two semantics: the semantics based on truth values and the semantics of proofs. Truth-based semantics is not rich enough to describe the computational aspects of proofs (in fact all proofs are interpreted into a unique truth value), while proofs semantics is not a semantics for logic: atomic formulae are not explicitly interpreted. Is there a general concept from which both semantics stem? Can we give an interpretation of logic starting from the interpretation of atomic formulae, rich enough to interpret also proofs?

Aim of this work is to prove that this general concept is chance. More precisely this work is an attempt on a mathematical analysis of the invariants of chance (or laws of chance) here described by true formulas of a suitable topos of presheaves constructed over the category of time, with the aim of showing that proofs are particular cases of these invariants. Here by proofs we mean proofs in linear logic.

Intuitively a law of chance is a property that remains stable, i.e. it is invariant w.r.t. information changes due to time and uncertainty.

Chance is defined in a universe of sets that vary over time and uncertainty, therefore time and uncertainty, in this work, are interwoven concepts.

For this reason it is necessary to extend the usual concept of time, because usual time (here called linear time) has not a clear link with uncertainty.

Time is described by a suitable category and it is linked to uncertainty so that what we usually call time appears as a set of arrows (a linear order) that describes the time path that is not affected by uncertainty.

In this perspective also the usual concept of truth can appear as a law of chance, in fact it remains stable w.r.t. time and uncertainty.

Although truth can be seen as a first approximation of a law of chance it is so elementary and mythological that it lost its link with the dynamic of the observables while here the laws of chance have a clear and operational link with the dynamic of observables, i.e. the flow of information. Indeed all the following analysis is founded on what here is called statistics.

A statistic is a method that given a set of observables computes a measure that describes the process in accordance with the observed data.

Observables are the outcomes of experiments and are defined as trajectories of suitable stochastic processes that describe the experiments.

It is assumed that to every atomic proposition we can associate an experiment constructed to test the property represented by the atomic proposition.

We will see that the experiments associated to atomic propositions can be combined giving compound experiments that define the connectives. Under these assumptions a statistic is defined as a method that, given a trajectory x, computes a measure s_x.

For example, if the experiment X is a coin tossing then to the trajectory x=hhtht (h for head and t for tail) we can associate the statistical measure s_x (h) = [3/5] and s_x (t) = [2/5].

Stochastic properties are described using sets of trajectories (stochastic cliques). For atomic propositions, stochastic cliques are sets of trajectories that give the same statistical measure. For instance the set {ht, hthhtt, htht} is a stochastic clique of the atomic proposition "the outcome is head" to which we associate to the coin tossing experiment.

In the above example, observables are used to approximate the unknown measure that governs the process, but they can be used in a dual way. In fact, in statistics a test is a method that uses the observables to exclude a measure.

For example if in 100 coin tosses we observe 98 tails, then we can use this observables to exclude the fact that the coin is fair, i.e. we can exclude the measure that gives the same probability to head and tail.

This duality is the key idea to define the negation and opens the door to logic. All the above properties are defined without any reference to the deductive algorithm (proofs) and are based only on some important properties of chance.

To discover the link between chance and logic we must shift from the usual semantics based on truth values to the proof semantics (Heyting and Kolmogorov).

After the discovery of the Curry-Howard isomorphism between proofs and typed l-calculus, a lot of work in logic and theoretical computer science has been done to give a semantics to proofs.

Many semantical environments for l-calculus have been studied, from Scott domains to coherent spaces that will be used in this work.

It will be proved that every proof can be interpreted in a stochastic clique that is defined using only the above properties of chance. This shows that the objects that describe the above stochastic properties are the same as those that describe proofs in the denotational semantics of logic.

The interest of Heyting-Kolmogorov semantics is to model proofs, therefore the interpretation of atomic formulas is irrelevant and hence neglected. In fact, in the letterature: "for atomic sentences, we assume that we know intrinsically what a proof is; for example, pencil and paper calculation serves as a proof of `27×37 =999"'.

Aim of this work is to show that the symmetries of logic are the symmetries of chance and the claim is that the link between logic and chance is rooted in the fact that proofs describe laws of chance.

To show this, we cannot "assume that we know intrinsically what a proof is" for atomic sentences, but atomic propositions must be interpreted into set of observables that describe some symmetries of chance and then it must be shown that proofs respect the laws of chance that govern the observables.

In fact, it will be proved that if p is a proof of f then the interpretation of p constructs the set of observables that satisfy the law of chance expressed by the proof of the formula f. In this sense we can say that proofs describe laws of chance that are satisfied by all the possible outcomes that belong to the interpretation of the proof.

Moreover it will be shown that the set of observables constructed by the proof of f is a law of chance, therefore it remains stable w.r.t. time and information changes.

In this semantics, validity is not defined using the abstract concept of truth but directly using sets of data that can be generated by an experiment.

The work is divided into two parts in the first part a stochastic interpretation of proofs is given, the second part is dedicated to the definition of law of chance, using a suitable topos of presheaves, and to show that proofs are laws of chance.

PDF

Date received: February 27, 2008