Да, мы предполагаем, что логика + теории первого порядка, такая как арифметика, является последовательной. Большинство математиков считают, что это так. Когда мы говорим о корректности Z3, мы рассматриваем алгоритмы и процедуры, использованные при его реализации, а не согласованность логической системы, на которой она основана. Наконец, как я указывал в своем ответе, доказательство правильности должно осуществляться в другой системе, которая «понимает» семантику C / C ++ (язык программирования, используемый для реализации Z3). Эта система может использовать другую логическую систему и даже может вызывать Z3 в качестве подпрограммы.

ибудь пробовал доказыватьZ3 с самим Z3?

Можно ли даже доказать, что Z3 является правильным, используя Z3?

Более теоретически, возможно ли доказать, что инструмент X является правильным, используя сам X?

Ответы на вопрос(2)

Ваш ответ на вопрос