کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4663181 | 1345234 | 2006 | 27 صفحه PDF | دانلود رایگان |
Deduction chains represent a syntactic and in a certain sense constructive method for proving completeness of a formal system. Given a formula ϕ, the deduction chains of ϕ are built up by systematically decomposing ϕ into its subformulae. In the case where ϕ is a valid formula, the decomposition yields a (usually cut-free) proof of ϕ. If ϕ is not valid, the decomposition produces a countermodel for ϕ. In the current paper, we extend this technique to a semiformal system for the Logic of Common Knowledge. The presence of fixed point constructs in this logic leads to potentially infinite-length deduction chains of a non-valid formula, in which case fairness of decomposition requires special attention. An adequate order of decomposition also plays an important role in the reconstruction of the proof of a valid formula from the set of its deduction chains.
Journal: Journal of Applied Logic - Volume 4, Issue 3, September 2006, Pages 331–357