User marco caminati - MathOverflow

Sequent calculus: is there a complete linear reasoning (i.e., no trees)?

2013-01-06T01:21:20Z

In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule.

If no inference rule has more than one premise, such a tree becomes a sequence: in a 1957 paper, Craig devised Linear Reasoning to pursue such an idea; an evolution of this approach (seemingly related to Craig's famous interpolation theorem, by the way) is exposed in the standard First-Order Logic textbook by Smullyan (chapter XVII in my edition).

The corresponding theorems, however, pose various restrictions: for example, on the form of the sentences involved.

Is linear reasoning possible in more general cases?

For example, is there a sequent calculus giving linear proofs and being simultaneously complete (and sound, of course) for classical first order logic? Or, on the contrary, is there some result limiting similar ambitions?

P.S.: I know about deep inference, so let us restrict to `standard' sequent calculi.

Background

When faced with the task of formalizing sequent calculus on a set theoretical proof assistant (Mizar), I felt trees would have been not so easy to actually work with, so I devised alternative frameworks. It worked, in the sense that one can manage not to ever mention trees and still carry on a great deal of results; however, they are still morally there, hence the question arose naturally.

Answer by Marco Caminati for Usage of set theory in undergraduate studies

2013-01-07T11:01:55Z

There are some kids with that wonderful attitude of asking "why?" about anything. The existence of a few syntactically simple axioms beyond which you cannot ask why anymore, as opposed to the discouraging "turtles all way down" approach, can be comforting to such minds, I think.

In these cases, I feel that the existence, and even the variety, of foundations should be mentioned, and made intriguing, early, which is a very delicate task.

The problem, of course, is that probably a child isn't generally prepared to face the rigors of formality, and the complexity of what there is between axioms and doing $2+2$.

This too often leads to never mentioning foundational issues, not even at college: I did physics at university and the most foundational stuff I was ever exposed to were the Cantor set, Dedekind cuts and $\epsilon / \delta$ definitions.

I think that in early education, the operational approach, as opposed to theoretical definitions, can be more appropriate, partly due to the fact that elementary school is expected by the adults to teach children how to perform numerical calculations. Later, however, when the confidence with the object one is manipulating all the time, at least the glimpse of foundations should be given: even only so that those interested can dig it. I sorely regret that didn't happen to me when I was younger, for example.

It is interesting that the opposite approach (heavy set theory from an early stage) was experimented in the past, and with little success: New Math.

Answer by Marco Caminati for How to tell a paradox from a "paradox"?

2012-09-26T14:34:39Z

Although I am not so good with philosophical subtleties, I have always found useful to make a distinction between an antinomy and a paradox. The first leads to a formal contradiction, i.e., a logical inconsistency in your theory (you can prove both a formula and its negation).

The second `merely' defies human intuition, without being a (known) antinomy. Much less worrying (ask Frege :)).

Many just use `paradox' for both things, but I find this highly confusing.

Answer by Marco Caminati for Interesting conjectures "discovered" by computers and proved by humans?

2012-03-25T09:55:47Z

You seem to be asking about computers formulating conjectures later proved by humans. As one not having had much exposure to the issue, I wonder how to teach a computer (maybe with some form of heuristics?) assessing it has found a plausible conjecture: in this case computer misses the comfort of knowing a result is true for it has proven it's true, while human mathematicians can use instinct or some kind of common sense. However, I found this:

A Symbolic Finite-State Approach For Automated Proving of Theorems in Combinatorial Game Theory

Answer by Marco Caminati for A book about model theory

2011-09-29T23:47:38Z

Rather than to a book, I point you to real formalizations in a set theory: I deem this appropriate given the question itself. Otherwise, downvote me please :)

I happen to have formalized in Mizar set theory (which is Tarski-Grothendieck, i.e. ZFC on steroids) the stuff you seem pointing to: language, wffs, interpretation, satisfaction relation, evaluation, sequent derivability, provability, etc...

In FOMODEL1: http://mizar.auburn.edu/version/current/html/fomodel1.html

you get most syntax (up to definition of atomic formula, or 0wff).

In FOMODEL2: http://mizar.auburn.edu/version/current/html/fomodel2.html

you will find the definition of satisfaction.

That is a series of five subsequent articles starting from scratch and getting to completeness theorem (and Lowenheim-Skolem, the latter only on my homepage, not submitted to Mizar people yet). The links point to hypertextual, proof-pruned versions. For full formalizations, look for the same files with the extension .miz in that same server.

Mizar formalizations are arguably among the most readable for the average mathematician (that's the factor that got myself started with it), that's why I thought you could find this stuff of some interest.

Answer by Marco Caminati for Pseudonyms of famous mathematicians

2010-11-08T19:06:03Z

At the height of fascist persecution of jews, Federigo Enriques penned some of his articles as Adriano Giovannini (reputedly coined from the names of his daughter Adriana and of his son Giovanni), as a device to circulate them. I was able to trace back to that pseudonym at least two papers: "Il pensiero di Galileo Galilei" and "L'errore nelle matematiche". As I understand it, that is to be considered a pseudonym used just in publications rather than a fully new name for real life, so I deemed the answer qualifying with regard to the question requirements.

Also, not being able to comment others' answers:

I can add von Neumann as good example of the category depicted in Andreas' answer.
As an anecdotal gloss to the Germain/Le Blanc case, it seems that even a century later that would have been a wise move: apparently Renato Caccioppoli was not so confident in women's mathematical capabilities, and it is said that once he ended examining a brilliant student of him with "Signorina, nonostante lei sia una donna le devo mettere 30 e lode.", which runs like: "Miss, despite you being a woman, it seems like I will have to give you A+".

Answer by Marco Caminati for What's the notation for a function restricted to a subset of the codomain?

2010-08-23T14:06:04Z

This would fit as a response to Harald Hanche-Olsen's remark, but I have not enough points for this.

Anyway, Mizar mathematial library chose exactly this notation; actually, it is introduced in the article on basic relations RELAT_1.MIZ, Def. 12, so it fits any relation and any set.

In a Mizar article you have just ASCII, so no subscripts, but you can always avoid ambiguities like f|X versus X|f by typing the two objects appearing in the notation as Relation and set respectively. I find interesting that what is expressible on paper by varying font size is emulated by typing in a proof checker.

Answer by Marco Caminati for Examples of great mathematical writing

2010-08-23T13:54:12Z

I wish someone had told me about this book when I was younger: A.I. Mal'cev, Algorithms and Recursive Functions.

The exposition is simple, thought provoking and rigorous. You are teased to delve into many strains when reading it.

Comment by Marco Caminati

2013-01-08T10:58:45Z

@mbsq: I'm sorry, but I just can't figure out what you mean by eternal and absolute math, so it's difficult to reply. I am interested to your point that you can pursue rigor without sticking to no "particular theory": how would you do that? To me, it sounds like saying that you can write a poem without using any particular alphabet. Anyway, reading my comments now, they sound a bit too polemical; I apologize for that.

Comment by Marco Caminati

2013-01-07T21:19:20Z

@mbsq-part two: The fact that multiple, particular choices to encode foundations exist should not mislead anyone into thinking that the results obtained by studying them (not only by applying them) are less "eternal" than the results you arbitrarily classify as such: your whole post is ultimately pivoted on such a subjective (and scarcely elaborated on) distinction. Finally, I find ironic that you deployed the fruits of reverse mathematics, arguably a foundational discipline, to dismiss the importance of foundational studies.

Comment by Marco Caminati

2013-01-07T21:19:07Z

@mbsq-part one: It seems to me that you have a merely utilitarian view of mathematical logic and foundational disciplines: as if they are "only" needed to attain consistency and rigor (which, by the way, is, in my opinion, as vital as creativity to mathematics: I dare to say that mathematics is a beautiful interplay between rigor and mental pure creation). What makes them even more exciting, to me at least, is that they are a beautiful subject of mathematical investigation themselves, giving them a special "double face" status.

Comment by Marco Caminati

2011-03-26T10:36:14Z

Following your remark, I soft-documented a bit about Caccioppoli, and now I embrace your interpretation of his (alleged) statement :)