# Return to Question

2 added 1502 characters in body

The link between logic and computation is stronger than ever, especially since the establishment of the Curry-Howard isomorphism specifying that `proofs` can be seen as `programs` and `formulas` as program's `types`.

I wondered if we could find any texts providing a philosophical viewpoint of the relation between logic and computation. I couldn't find any document about that.

Moreover, I have some related questions :

1) Since most logical systems (e.g intuitionnistic natural deduction, classical sequent calculus) corresponds to computational systems (e.g simply typed λ-calculus, system F, combinatory logic...), can we say that logic and computation have the same nature and origin ? A lot of difficulties arised from the question of the nature of Logic, does computation give an answer ?

2) Can we say that any system which doesn't share computational properties with a computational system is not "a logic" ? (e.g no cut elimination theorem, no confluence/church-rosser property)

EDIT : After some research

The only things I could find were the work of the french group LIGC but most of the articles they write are in french only.

It seems that most of the works linking philosophy and computation concern Linear Logic (which emerges from the Curry-Howard isomorphism) and the Lambda-Calculus (which give a formal account to [functional] computer programs).

If I'm not wrong, Linear Logic takes computation (cut-rule elimination seen as evaluation of programs) as a basis for logic. Some properties on programs such that the cut-elimination theorem, confluence or the church-rosser property, when taking the point of view of logic, ensure that our logic behave in a coherent way. We rely on the operational behaviour of logic rather than language or purely philosophical foundations.

It seems that these work haven't reached the english community yet but maybe one can find some articles in english written by the members of the group.

Some not-too-technical papers (unfortunately in french) :

The link between logic and computation is stronger than ever, especially since the establishment of the Curry-Howard isomorphism specifying that `proofs` can be seen as `programs` and `formulas` as program's `types`.

I wondered if we could find any texts providing a philosophical viewpoint of the relation between logic and computation. I couldn't find any document about that.

Moreover, I have some related questions :

1) Since most logical systems (e.g intuitionnistic natural deduction, classical sequent calculus) corresponds to computational systems (e.g simply typed λ-calculus, system F, combinatory logic...), can we say that logic and computation have the same nature and origin ? A lot of difficulties arised from the question of the nature of Logic, does computation give an answer ?

2) Can we say that any system which doesn't share computational properties with a computational system is not "a logic" ? (e.g no cut elimination theorem, no confluence/church-rosser property)

The link between logic and computation is stronger than ever, especially since the establishment of the Curry-Howard isomorphism specifying that `proofs` can be seen as `programs` and `formulas` as program's `types`.

I wondered if we could find any texts providing a philosophical viewpoint of the relation between logic and computation. I couldn't find any document about that.

Moreover, I have some related questions :

1) Since most logical systems (e.g intuitionnistic natural deduction, classical sequent calculus) corresponds to computational systems (e.g simply typed λ-calculus, system F, combinatory logic...), can we say that logic and computation have the same nature and origin ? A lot of difficulties arised from the question of the nature of Logic, does computation give an answer ?

2) Can we say that any system which doesn't share computational properties with a computational system is not "a logic" ? (e.g no cut elimination theorem, no confluence/church-rosser property)

EDIT : After some research

The only things I could find were the work of the french group LIGC but most of the articles they write are in french only.

It seems that most of the works linking philosophy and computation concern Linear Logic (which emerges from the Curry-Howard isomorphism) and the Lambda-Calculus (which give a formal account to [functional] computer programs).

If I'm not wrong, Linear Logic takes computation (cut-rule elimination seen as evaluation of programs) as a basis for logic. Some properties on programs such that the cut-elimination theorem, confluence or the church-rosser property, when taking the point of view of logic, ensure that our logic behave in a coherent way. We rely on the operational behaviour of logic rather than language or purely philosophical foundations.

It seems that these work haven't reached the english community yet but maybe one can find some articles in english written by the members of the group.

Some not-too-technical papers (unfortunately in french) :

Tweeted twitter.com/StackPhilosophy/status/862488789603819520
1

# Logic and Computation : a philosophical viewpoint

The link between logic and computation is stronger than ever, especially since the establishment of the Curry-Howard isomorphism specifying that `proofs` can be seen as `programs` and `formulas` as program's `types`.

I wondered if we could find any texts providing a philosophical viewpoint of the relation between logic and computation. I couldn't find any document about that.

Moreover, I have some related questions :

1) Since most logical systems (e.g intuitionnistic natural deduction, classical sequent calculus) corresponds to computational systems (e.g simply typed λ-calculus, system F, combinatory logic...), can we say that logic and computation have the same nature and origin ? A lot of difficulties arised from the question of the nature of Logic, does computation give an answer ?

2) Can we say that any system which doesn't share computational properties with a computational system is not "a logic" ? (e.g no cut elimination theorem, no confluence/church-rosser property)