5 replaced http://philosophy.stackexchange.com/ with https://philosophy.stackexchange.com/
source | link

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also http://philosophy.stackexchange.com/questions/24885/why-is-tarskis-notion-of-logical-validity-preferred-to-deductive-oneWhy is Tarski's notion of logical validity preferred to deductive one? I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also http://philosophy.stackexchange.com/questions/24885/why-is-tarskis-notion-of-logical-validity-preferred-to-deductive-one I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also Why is Tarski's notion of logical validity preferred to deductive one? I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

4 edited body
source | link

The "founding act of modern logic" is Frege's predicate calculus with logical consequence based on semantics. This last part, a.k.a. "realism", is, according to Girard, fatally flawed. Here are some of thehis reasons why:

The "founding act of modern logic" is Frege's predicate calculus with logical consequence based on semantics. This last part, a.k.a. "realism", is, according to Girard, fatally flawed. Here are some of the reasons why:

The "founding act of modern logic" is Frege's predicate calculus with logical consequence based on semantics. This last part, a.k.a. "realism", is, according to Girard, fatally flawed. Here are some of his reasons why:

3 added 135 characters in body
source | link

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "one interprets the language by the same thing""there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also http://philosophy.stackexchange.com/questions/24885/why-is-tarskis-notion-of-logical-validity-preferred-to-deductive-one I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

The distinction on which Fregean logic is "derelict" can perhaps be manifested differently. I can only speculate that "analytic substrate" probably refers to the substrate of Girard's self-sufficient language, and "performative"/"declarative" dichotomy is related to the two sides of Curry-Howard correspondence between logical proofs and typed λ-terms, "execution" and "construction". This is the basis of Girard's idea of justifying syntax from within syntax, by uncovering (Kant inspired) conditions of the possibility of its practical functioning without infinite loops. On this I find Abrusci-Pistone's expose of Girard's program somewhat easier to follow :

"Research on typed λ-calculi usually privileges, indeed, an approach directed to the dynamical features of logic: proofs, as isomorphic with programs, are taken as mathematical objects that must not only be constructed following the rules, but also be executed following the dynamics of those rules. The duality construction/execution is made explicit by the so-called formulae-as-types correspondence, by which logical formulas are associated with types, that is, with sets of proofs satisfying the norms associated by logical rules to those formulas... Logical syntax can thus be seen both as a constructive tool, enabling the formation of (normalizing) typed terms, and as a constraining one, imposing a custom on pure terms (and their socialization) in order to force termination. In analogy with Kant’s transcendentalism, indeed, the program tries to raise the issue to deduct, that is, to legitimize the authority exercised by logical languages... without reference to those entities whose representability crucially relies on the use of what is charged of being justified."

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "one interprets the language by the same thing". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also http://philosophy.stackexchange.com/questions/24885/why-is-tarskis-notion-of-logical-validity-preferred-to-deductive-one I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

I can only speculate that "analytic substrate" probably refers to the substrate of Girard's self-sufficient language, and "performative"/"declarative" dichotomy is related to the two sides of Curry-Howard correspondence between logical proofs and typed λ-terms, "execution" and "construction". This is the basis of Girard's idea of justifying syntax from within syntax, by uncovering (Kant inspired) conditions of the possibility of its practical functioning without infinite loops. On this I find Abrusci-Pistone's expose of Girard's program somewhat easier to follow :

"Research on typed λ-calculi usually privileges, indeed, an approach directed to the dynamical features of logic: proofs, as isomorphic with programs, are taken as mathematical objects that must not only be constructed following the rules, but also be executed following the dynamics of those rules. The duality construction/execution is made explicit by the so-called formulae-as-types correspondence, by which logical formulas are associated with types, that is, with sets of proofs satisfying the norms associated by logical rules to those formulas... Logical syntax can thus be seen both as a constructive tool, enabling the formation of (normalizing) typed terms, and as a constraining one, imposing a custom on pure terms (and their socialization) in order to force termination."

On my reading, in the quote Girard is pointing out that "realists" can not distinguish ⊢ from ⇒, or rather that their distinction is purely contextual (language vs. metalanguage) rather than substantive. The reason is that "there is no ultimate reality the language is referring to". This makes Fregean logic (and by extension all of its modern successors) "derelict". On ⇒ specifically Girard contrasts proof theoretic interpretation of A ⇒ B as a function that sends proofs of A to proofs of B, to the Tarskian tautology that it is true when the truth of A implies the truth of B, commenting that "such a truism may sometimes be useful, but it is clearly meaningless: tarskian truth is a classified topic". See also http://philosophy.stackexchange.com/questions/24885/why-is-tarskis-notion-of-logical-validity-preferred-to-deductive-one I do not see, however, that he necessarily wants to rehabilitate ⊢, which presupposes stepping outside of language to "perform" logic, something Girard denounces:

The distinction on which Fregean logic is "derelict" can perhaps be manifested differently. I can only speculate that "analytic substrate" probably refers to the substrate of Girard's self-sufficient language, and "performative"/"declarative" dichotomy is related to the two sides of Curry-Howard correspondence between logical proofs and typed λ-terms, "execution" and "construction". This is the basis of Girard's idea of justifying syntax from within syntax, by uncovering (Kant inspired) conditions of the possibility of its practical functioning without infinite loops. On this I find Abrusci-Pistone's expose of Girard's program somewhat easier to follow :

"Research on typed λ-calculi usually privileges, indeed, an approach directed to the dynamical features of logic: proofs, as isomorphic with programs, are taken as mathematical objects that must not only be constructed following the rules, but also be executed following the dynamics of those rules. The duality construction/execution is made explicit by the so-called formulae-as-types correspondence, by which logical formulas are associated with types, that is, with sets of proofs satisfying the norms associated by logical rules to those formulas... Logical syntax can thus be seen both as a constructive tool, enabling the formation of (normalizing) typed terms, and as a constraining one, imposing a custom on pure terms (and their socialization) in order to force termination. In analogy with Kant’s transcendentalism, indeed, the program tries to raise the issue to deduct, that is, to legitimize the authority exercised by logical languages... without reference to those entities whose representability crucially relies on the use of what is charged of being justified."

2 added 135 characters in body
source | link
1
source | link