A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic (Q1064322): Difference between revisions
From MaRDI portal
Removed claims |
ReferenceBot (talk | contribs) Changed an Item |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / author | |||
Property / author: Victor N. Krivtsov / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Roman Kossak / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5798786 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5839919 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Non-null implication / rank | |||
Normal rank |
Latest revision as of 19:09, 14 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic |
scientific article |
Statements
A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic (English)
0 references
1984
0 references
A system of natural deduction for a negationless arithmetic is presented. A deduction in \(HA^ N\) is defined as a pair of deductions \(<\Sigma_ 1,\Sigma_ 2>\), where \(\Sigma_ 1\) is a proof of nonemptiness of the conjunction of all open hypotheses of \(\Sigma_ 2\) and \(\Sigma_ 2\) is a deduction in a classical sense. Natural interpretations of HA in \(HA^ N\) and \(HA^ N\) in HA are introduced. Appropriate interpretation results are proven showing in particular that HA is a conservative extension of \(HA^ N\) with respect to the interpretation.
0 references
natural deduction
0 references
interpretation
0 references