Was bedeutet in Isabelle?

Question

(Dies ist so ziemlich eine logische Frage.) ⋀ wie in ⋀y . Py scheint eine Art Platzhalter zu sein. Es tritt nach der Verwendung von apply (rule allI) oder apply (erule exE auf. Zuerst dachte ich, es sei wie ein Vortäuschen because, wegen der Regel allI, die (!!x. Px) => ∀x. Px ist (ich glaube, dass !! verwendet wird, um ⋀ an der Stelle darzustellen, von der ich das bekam). Aber ich schien nicht in der Lage zu sein, allI in bestimmten Szenarien anzuwenden, die dieser Regel zu entsprechen schienen. Was bedeutet ⋀ wirklich? Ich frage mich, ob ⋀ unterschiedliche Dinge in verschiedenen Situationen bedeuten kann.

Answer 1

⋀ ist ein universeller Quantifizierer, ja, aber es ist die metalogische eins. I.e. dasjenige, mit dem Sie die Logik beschreiben, in der Sie arbeiten, einschließlich ∀. In ähnlicher Weise ist der metalogische Implikationsoperator. Und das sind die einzigen beiden Primitiven von Isabelles Metalogie; es gibt keine Negation, also ist es viel schwächer als die klassische Logik. Weitere Informationen finden Sie unter http://isabelle.in.tum.de/coursematerial/PSV2009-1/session2/document.pdf oder https://www.cl.cam.ac.uk/teaching/1011/L21/5%20-%20Logic.pdf.