Timeline for Completeness of certain formal deduction system
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Jun 5, 2020 at 14:03 | comment | added | Emil Jeřábek | Ok. Then I do not see how to either prove or disprove completeness. | |
| Jun 5, 2020 at 13:28 | comment | added | Evgeny Kuznetsov | You are right, I want to figure out if it is possible to prove completeness without replacement of a sub-formulas but with substitution if needed. | |
| Jun 5, 2020 at 13:10 | comment | added | Emil Jeřábek | That does not answer what I asked. Can the tautological rules be applied only to whole formulas, or also to subformulas? | |
| Jun 5, 2020 at 13:09 | comment | added | Evgeny Kuznetsov | @Emil Jeřábek Yes, you see it correctly, tautological rules work both direction. How do we see completeness of the calculus? | |
| Jun 1, 2020 at 15:37 | comment | added | Emil Jeřábek | What exactly do you mean by “tautological rules”? I assumed, as the notation suggests, that these are just inference rules that can be applied in both directions (on whole lines in the proof). However, do you by any chance mean that they can be actually applied as replacement rules anywhere deep inside the formulas? If the latter, then the calculus is easily seen to be complete. | |
| Jun 1, 2020 at 13:53 | comment | added | Evgeny Kuznetsov | This is a system we usually offer to students in first common logic course for students of non-mathematical profile, in order they understand what is concept of proof. | |
| Jun 1, 2020 at 12:54 | comment | added | Emil Jeřábek | Where does the system come from? | |
| Jun 1, 2020 at 12:15 | history | asked | Evgeny Kuznetsov | CC BY-SA 4.0 |