Skip to main content
MathOverflow

Return to Question

replaced http://mathoverflow.net/ with https://mathoverflow.net/
Source Link
Community Bot
Community Bot
  • 1
  • 2
  • 3

In the answers to this questionthis question, Timothy Gowers asks:

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning?

One answer to this question is given by Fredkin and Toffoli's conservative logic, which is an attempt to give a system of digital logic consistent with various abstract physical principles such as conservation laws, reversibility, and one-to-one composition (ie, no unbounded fanout, since signal strength degrades when signals are split). However, to a proof theorist, the constraints they describe sound hauntingly similar to the language used to motivate linear logic. Furthemore, the circuit diagrams they draw look like string diagrams in monoidal categories, which are models of linear logic.

So my own question is, how is conservative logic related to linear logic?

In the answers to this question, Timothy Gowers asks:

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning?

One answer to this question is given by Fredkin and Toffoli's conservative logic, which is an attempt to give a system of digital logic consistent with various abstract physical principles such as conservation laws, reversibility, and one-to-one composition (ie, no unbounded fanout, since signal strength degrades when signals are split). However, to a proof theorist, the constraints they describe sound hauntingly similar to the language used to motivate linear logic. Furthemore, the circuit diagrams they draw look like string diagrams in monoidal categories, which are models of linear logic.

So my own question is, how is conservative logic related to linear logic?

In the answers to this question, Timothy Gowers asks:

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning?

One answer to this question is given by Fredkin and Toffoli's conservative logic, which is an attempt to give a system of digital logic consistent with various abstract physical principles such as conservation laws, reversibility, and one-to-one composition (ie, no unbounded fanout, since signal strength degrades when signals are split). However, to a proof theorist, the constraints they describe sound hauntingly similar to the language used to motivate linear logic. Furthemore, the circuit diagrams they draw look like string diagrams in monoidal categories, which are models of linear logic.

So my own question is, how is conservative logic related to linear logic?

Source Link
Neel Krishnaswami
Neel Krishnaswami
  • 9.2k
  • 1
  • 30
  • 54

How is Fredkin and Toffoli's Conservative Logic related to Linear Logic?

In the answers to this question, Timothy Gowers asks:

I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question rather than an answer. (I'm interested in the answers that have already been given though.) My question is this. Is there a system of logic that will allow us to prove only statements that have physical meaning?

One answer to this question is given by Fredkin and Toffoli's conservative logic, which is an attempt to give a system of digital logic consistent with various abstract physical principles such as conservation laws, reversibility, and one-to-one composition (ie, no unbounded fanout, since signal strength degrades when signals are split). However, to a proof theorist, the constraints they describe sound hauntingly similar to the language used to motivate linear logic. Furthemore, the circuit diagrams they draw look like string diagrams in monoidal categories, which are models of linear logic.

So my own question is, how is conservative logic related to linear logic?